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

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