let X, Y be RealLinearSpace; :: thesis: MultilinearOperators (<*X*>,Y) = LinearOperators ((product <*X*>),Y)
for f being object holds
( f in MultilinearOperators (<*X*>,Y) iff f in LinearOperators ((product <*X*>),Y) )

proof

let f be object ; :: thesis: ( f in MultilinearOperators (<*X*>,Y) iff f in LinearOperators ((product <*X*>),Y) )
( f is LinearOperator of (product <*X*>),Y iff f is MultilinearOperator of <*X*>,Y ) by Th9;
hence ( f in MultilinearOperators (<*X*>,Y) iff f in LinearOperators ((product <*X*>),Y) ) by LOPBAN_1:def 6, LOPBAN10:def 4; :: thesis: verum

end;

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