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