let X, Y be RealNormSpace; :: thesis: BoundedMultilinearOperators (<*X*>,Y) = BoundedLinearOperators ((product <*X*>),Y)
for f being object holds
( f in BoundedMultilinearOperators (<*X*>,Y) iff f in BoundedLinearOperators ((product <*X*>),Y) )

proof

let f be object ; :: thesis: ( f in BoundedMultilinearOperators (<*X*>,Y) iff f in BoundedLinearOperators ((product <*X*>),Y) )
( f is Lipschitzian LinearOperator of (product <*X*>),Y iff f is Lipschitzian MultilinearOperator of <*X*>,Y ) by Th21;
hence ( f in BoundedMultilinearOperators (<*X*>,Y) iff f in BoundedLinearOperators ((product <*X*>),Y) ) by LOPBAN_1:def 9, LOPBAN10:def 11; :: thesis: verum

end;

hence BoundedMultilinearOperators (<*X*>,Y) = BoundedLinearOperators ((product <*X*>),Y) by TARSKI:2; :: thesis: verum