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