reconsider I = I as Interpreter of S,U by Def4;
I . s is Interpreter of s,U by Def3;
hence I . s is Interpreter of s,U ; :: thesis: verum