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

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

assume f is Lipschitzian LinearOperator of (product <*X*>),Y ; :: thesis: f is Lipschitzian MultilinearOperator of <*X*>,Y
then reconsider f0 = f as Lipschitzian 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 z being Element of X holds (reproj (i,s)) . z = (IsoCPNrSP X) . z

proof

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

end;

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

end;

then reconsider f1 = f0 as MultilinearOperator of <*X*>,Y by LOPBAN10:def 6;
consider M being Real such that
A9: ( 0 <= M & ( for x being VECTOR of (product <*X*>) holds ||.(f0 . x).|| <= M * ||.x.|| ) ) by LOPBAN_1:def 8;

now :: thesis: for x being VECTOR of (product <*X*>) holds ||.(f1 . x).|| <= M * (NrProduct x)

let x be VECTOR of (product <*X*>); :: thesis: ||.(f1 . x).|| <= M * (NrProduct x)
NrProduct x = ||.x.|| by Th19;
hence ||.(f1 . x).|| <= M * (NrProduct x) by A9; :: thesis: verum

end;

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

end;

assume f is Lipschitzian MultilinearOperator of <*X*>,Y ; :: thesis: f is Lipschitzian LinearOperator of (product <*X*>),Y
then reconsider f0 = f as Lipschitzian MultilinearOperator of <*X*>,Y ;
reconsider i = 1 as Element of dom <*X*> by A1, TARSKI:def 1;
set s = the Element of (product <*X*>);
A10: reproj (i, the Element of (product <*X*>)) = IsoCPNrSP X by Th18;
reconsider g = f0 * (IsoCPNrSP X) as LinearOperator of X,Y by A10, LOPBAN10:def 6;
consider M being Real such that
A11: ( 0 <= M & ( for x being Point of (product <*X*>) holds ||.(f0 . x).|| <= M * (NrProduct x) ) ) by LOPBAN10:def 10;

now :: thesis: for x being VECTOR of X holds ||.(g . x).|| <= M * ||.x.||

let x be VECTOR of X; :: thesis: ||.(g . x).|| <= M * ||.x.||
reconsider s = <*x*> as Point of (product <*X*>) by Th12;
A12: g . x = f0 . ((IsoCPNrSP X) . x) by FUNCT_2:15
.= f0 . s by Def2 ;
NrProduct s = ||.s.|| by Th19
.= ||.x.|| by Th12 ;
hence ||.(g . x).|| <= M * ||.x.|| by A11, A12; :: thesis: verum

end;

then g is Lipschitzian by A11, LOPBAN_1:def 8;
hence f is Lipschitzian LinearOperator of (product <*X*>),Y by Th17; :: thesis: verum