let X, Y be ComplexNormSpace; :: thesis: for f being bounded LinearOperator of X,Y holds modetrans (f,X,Y) = f
let f be bounded LinearOperator of X,Y; :: thesis: modetrans (f,X,Y) = f
f in BoundedLinearOperators (X,Y) by Def8;
hence modetrans (f,X,Y) = f by Def10; :: thesis: verum