let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace
for f being Lipschitzian MultilinearOperator of X,Y holds modetrans (f,X,Y) = f
let Y be RealNormSpace; :: thesis: for f being Lipschitzian MultilinearOperator of X,Y holds modetrans (f,X,Y) = f
let f be Lipschitzian MultilinearOperator of X,Y; :: thesis: modetrans (f,X,Y) = f
f in BoundedMultilinearOperators (X,Y) by Def9;
hence modetrans (f,X,Y) = f by Def11; :: thesis: verum