let X, Y be ComplexNormSpace; :: 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 Def7;
hence modetrans (f,X,Y) = f by Def9; :: thesis: verum