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