let X, Y, Z be RealNormSpace; :: thesis: for f being Lipschitzian BilinearOperator of X,Y,Z holds modetrans (f,X,Y,Z) = f
let f be Lipschitzian BilinearOperator of X,Y,Z; :: thesis: modetrans (f,X,Y,Z) = f
f in BoundedBilinearOperators (X,Y,Z) by Def9;
hence modetrans (f,X,Y,Z) = f by Def11; :: thesis: verum