let X, Y be RealNormSpace; :: thesis: for f being Lipschitzian LinearOperator of X,Y holds modetrans (f,X,Y) = f
let f be Lipschitzian LinearOperator of X,Y; :: thesis: modetrans (f,X,Y) = f
f in BoundedLinearOperators (X,Y) by Def9;
hence modetrans (f,X,Y) = f by Def11; :: thesis: verum