let X, Y be RealNormSpace; :: 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 Def10;
hence modetrans f,X,Y = f by Def12; :: thesis: verum