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

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