let X, Y be RealLinearSpace; :: thesis: for f being object holds
( f is LinearOperator of (product <*X*>),Y iff f is MultilinearOperator of <*X*>,Y )
let f be object ; :: thesis: ( f is LinearOperator of (product <*X*>),Y iff f is MultilinearOperator of <*X*>,Y )
A1: dom <*X*> = {1} by FINSEQ_1:2, FINSEQ_1:38;

hereby :: thesis: ( f is MultilinearOperator of <*X*>,Y implies f is LinearOperator of (product <*X*>),Y )

assume f is LinearOperator of (product <*X*>),Y ; :: thesis: f is MultilinearOperator of <*X*>,Y
then reconsider f0 = f as LinearOperator of (product <*X*>),Y ;
for i being Element of dom <*X*>
for s being Element of (product <*X*>) holds f0 * (reproj (i,s)) is LinearOperator of (<*X*> . i),Y

proof

let i be Element of dom <*X*>; :: thesis: for s being Element of (product <*X*>) holds f0 * (reproj (i,s)) is LinearOperator of (<*X*> . i),Y
let s be Element of (product <*X*>); :: thesis: f0 * (reproj (i,s)) is LinearOperator of (<*X*> . i),Y
A2: i = 1 by A1, TARSKI:def 1;
then A3: <*X*> . i = X ;
for x being Element of X holds (reproj (i,s)) . x = (IsoCPRLSP X) . x

proof

let x be Element of X; :: thesis: (reproj (i,s)) . x = (IsoCPRLSP X) . x
s in the carrier of (product <*X*>) ;
then s in rng (IsoCPRLSP X) by FUNCT_2:def 3;
then consider x0 being object such that
A4: ( x0 in the carrier of X & s = (IsoCPRLSP X) . x0 ) by FUNCT_2:11;
reconsider x0 = x0 as Point of X by A4;
A5: (IsoCPRLSP X) . x0 = <*x0*> by Def1;
A6: dom s = Seg 1 by A4, A5, FINSEQ_1:38;
dom (s +* (i,x)) = dom s by FUNCT_7:30
.= Seg 1 by A4, A5, FINSEQ_1:38 ;
then A7: len (s +* (i,x)) = 1 by FINSEQ_1:def 3;
A8: (s +* (i,x)) . 1 = x by A1, A2, A6, FINSEQ_1:2, FUNCT_7:31;
thus (reproj (i,s)) . x = s +* (i,x) by A3, Th1
.= <*x*> by A7, A8, FINSEQ_1:40
.= (IsoCPRLSP X) . x by Def1 ; :: thesis: verum

end;

then reproj (i,s) = IsoCPRLSP X by A3;
hence f0 * (reproj (i,s)) is LinearOperator of (<*X*> . i),Y by A3, Th7; :: thesis: verum

end;

hence f is MultilinearOperator of <*X*>,Y by LOPBAN10:def 3; :: thesis: verum

end;

assume f is MultilinearOperator of <*X*>,Y ; :: thesis: f is LinearOperator of (product <*X*>),Y
then reconsider f1 = f as MultilinearOperator of <*X*>,Y ;
reconsider i = 1 as Element of dom <*X*> by A1, TARSKI:def 1;
set s = the Element of (product <*X*>);
A9: reproj (i, the Element of (product <*X*>)) = IsoCPRLSP X by Th8;
f1 * (reproj (i, the Element of (product <*X*>))) is LinearOperator of (<*X*> . i),Y by LOPBAN10:def 3;
hence f is LinearOperator of (product <*X*>),Y by A9, Th7; :: thesis: verum