let X, Z be RealNormSpace; :: thesis:
let Y be RealNormSpace-Sequence; :: thesis:
set CX = the carrier of X;
set CY = carr Y;
set CZ = the carrier of Z;
consider J being Function of (Funcs ( the carrier of X,(Funcs ((product (carr Y)), the carrier of Z)))),(Funcs ((product ((carr Y) ^ <* the carrier of X*>)), the carrier of Z)) such that
A1: ( J is bijective & ( for f being Function of the carrier of X,(Funcs ((product (carr Y)), the carrier of Z))
for y being FinSequence
for x being object st y in product (carr Y) & x in the carrier of X holds
(J . f) . (y ^ <*x*>) = (f . x) . y ) ) by NDIFF_6:6;
set LXYZ = the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z))));
set BXYZ = the carrier of (R_NormSpace_of_BoundedMultilinearOperators ((Y ^ <*X*>),Z));
set LYZ = the carrier of (R_NormSpace_of_BoundedMultilinearOperators (Y,Z));
product <*X*> = NORMSTR(# (product (carr <*X*>)),(zeros <*X*>),[:(addop <*X*>):],[:(multop <*X*>):],(productnorm <*X*>) #) by PRVECT_2:6;
then A2: the carrier of (product <*X*>) = product <* the carrier of X*> by Th31;
A3: product Y = NORMSTR(# (product (carr Y)),(zeros Y),[:(addop Y):],[:(multop Y):],(productnorm Y) #) by PRVECT_2:6;
A4: the carrier of (R_NormSpace_of_BoundedMultilinearOperators (Y,Z)) c= Funcs ((product (carr Y)), the carrier of Z) by A3, XBOOLE_1:1;
A5: the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))) c= Funcs ( the carrier of X, the carrier of (R_NormSpace_of_BoundedMultilinearOperators (Y,Z))) by XBOOLE_1:1;
product (Y ^ <*X*>) = NORMSTR(# (product (carr (Y ^ <*X*>))),(zeros (Y ^ <*X*>)),[:(addop (Y ^ <*X*>)):],[:(multop (Y ^ <*X*>)):],(productnorm (Y ^ <*X*>)) #) by PRVECT_2:6;
then A6: the carrier of (product (Y ^ <*X*>)) = product ((carr Y) ^ (carr <*X*>)) by Th30
.= product ((carr Y) ^ <* the carrier of X*>) by Th31 ;
Funcs ( the carrier of X, the carrier of (R_NormSpace_of_BoundedMultilinearOperators (Y,Z))) c= Funcs ( the carrier of X,(Funcs ((product (carr Y)), the carrier of Z)))

proof

let f be object ; :: according to TARSKI:def 3 :: thesis:
assume f in Funcs ( the carrier of X, the carrier of (R_NormSpace_of_BoundedMultilinearOperators (Y,Z))) ; :: thesis:
then consider f1 being Function such that
A7: ( f = f1 & dom f1 = the carrier of X & rng f1 c= the carrier of (R_NormSpace_of_BoundedMultilinearOperators (Y,Z)) ) by FUNCT_2:def 2;
rng f1 c= Funcs ((product (carr Y)), the carrier of Z) by A4, A7, XBOOLE_1:1;
hence f in Funcs ( the carrier of X,(Funcs ((product (carr Y)), the carrier of Z))) by A7, FUNCT_2:def 2; :: thesis:

end;

proof

let f be Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))); :: thesis:
A10: I . f = J . f by FUNCT_1:49;
A11: f in Funcs ( the carrier of X,(Funcs ((product (carr Y)), the carrier of Z))) by A8, TARSKI:def 3;
reconsider f0 = f as Function of the carrier of X,(Funcs ((product (carr Y)), the carrier of Z)) by A8, TARSKI:def 3, FUNCT_2:66;
reconsider f1 = f as Lipschitzian LinearOperator of X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)) by LOPBAN_1:def 9;
thus A12: for x being Point of X ex g being Lipschitzian MultilinearOperator of Y,Z st
( g = f . x & ( for y being Point of (product Y) holds (I . f) . (y ^ <*x*>) = g . y ) ) :: thesis:

proof

let x be Point of X; :: thesis:
f1 . x in BoundedMultilinearOperators (Y,Z) ;
then reconsider g = f0 . x as Lipschitzian MultilinearOperator of Y,Z by LOPBAN10:def 11;
take g ; :: thesis:
thus g = f . x ; :: thesis:
let y be Point of (product Y); :: thesis:
thus (I . f) . (y ^ <*x*>) = g . y by A1, A3, A10; :: thesis:

end;

A13: J . f is Function of (product ((carr Y) ^ <* the carrier of X*>)), the carrier of Z by A11, FUNCT_2:5, FUNCT_2:66;
reconsider Jf = J . f as Function of (product (Y ^ <*X*>)),Z by A6, A11, FUNCT_2:5, FUNCT_2:66;
for i being Element of dom (Y ^ <*X*>)
for z being Element of (product (Y ^ <*X*>)) holds Jf * (reproj (i,z)) is LinearOperator of ((Y ^ <*X*>) . i),Z

proof

let i be Element of dom (Y ^ <*X*>); :: thesis:
let z be Element of (product (Y ^ <*X*>)); :: thesis:
consider y, px being FinSequence such that
A14: ( z = y ^ px & y in product (carr Y) & px in product <* the carrier of X*> ) by RLAFFIN3:2, A6;
reconsider y = y as Point of (product Y) by A3, A14;
consider x being Point of X such that
A15: px = <*x*> by A2, A14, Th12;
consider cy being Function such that
A16: ( y = cy & dom cy = dom (carr Y) & ( for i being object st i in dom (carr Y) holds
cy . i in (carr Y) . i ) ) by A14, CARD_3:def 5;
A17: dom cy = Seg (len (carr Y)) by A16, FINSEQ_1:def 3;
reconsider cy = cy as FinSequence by A16;
A18: len y = len (carr Y) by A16, A17, FINSEQ_1:def 3
.= len Y by PRVECT_1:def 11 ;
A19: dom (Y ^ <*X*>) = Seg (len (Y ^ <*X*>)) by FINSEQ_1:def 3
.= Seg ((len Y) + (len <*X*>)) by FINSEQ_1:22
.= Seg ((len Y) + 1) by FINSEQ_1:40 ;
A20: ( 1 <= i & i <= (len Y) + 1 ) by A19, FINSEQ_1:1;

per cases ;

suppose i <= len y ; :: thesis:

then i in Seg (len Y) by A18, A20;
then reconsider i0 = i as Element of dom Y by FINSEQ_1:def 3;
consider g being Lipschitzian MultilinearOperator of Y,Z such that
A21: ( g = f . x & ( for py being Point of (product Y) holds (I . f) . (py ^ <*x*>) = g . py ) ) by A12;
A22: (Y ^ <*X*>) . i = Y . i0 by FINSEQ_1:def 7;
then reconsider L = Jf * (reproj (i,z)) as Function of (Y . i0),Z ;
dom (I . f) = the carrier of (product (Y ^ <*X*>)) by A6, A10, A13, FUNCT_2:def 1;
then rng (reproj (i,z)) c= dom (I . f) ;
then A23: dom ((I . f) * (reproj (i,z))) = dom (reproj (i,z)) by RELAT_1:27
.= the carrier of ((Y ^ <*X*>) . i) by FUNCT_2:def 1 ;
A24: dom (g * (reproj (i0,y))) = the carrier of (Y . i0) by FUNCT_2:def 1;
for w being object st w in dom ((I . f) * (reproj (i,z))) holds
((I . f) * (reproj (i,z))) . w = (g * (reproj (i0,y))) . w

proof

let w be object ; :: thesis:
assume A25: w in dom ((I . f) * (reproj (i,z))) ; :: thesis:
then reconsider w1 = w as Point of ((Y ^ <*X*>) . i) ;
reconsider w2 = w as Point of (Y . i0) by A25, FINSEQ_1:def 7;
A26: (reproj (i,z)) . w1 = ((reproj (i0,y)) . w2) ^ <*x*> by A14, A15, Th32;
thus ((I . f) * (reproj (i,z))) . w = (I . f) . ((reproj (i,z)) . w1) by FUNCT_2:15
.= g . ((reproj (i0,y)) . w2) by A21, A26
.= (g * (reproj (i0,y))) . w by FUNCT_2:15 ; :: thesis:

end;

then (I . f) * (reproj (i,z)) = g * (reproj (i0,y)) by A22, A23, A24, FUNCT_1:2;
hence Jf * (reproj (i,z)) is LinearOperator of ((Y ^ <*X*>) . i),Z by A10, A22, LOPBAN10:def 6; :: thesis:

end;

suppose len y < i ; :: thesis:

then A28: (len y) + 1 <= i by NAT_1:13;
then A29: i = (len y) + 1 by A20, A18, XXREAL_0:1;
then A30: (Y ^ <*X*>) . i = X by A18, FINSEQ_1:42;
then reconsider h = Jf * (reproj (i,z)) as Function of X,Z ;
A31: dom (reproj (i,z)) = the carrier of ((Y ^ <*X*>) . i) by FUNCT_2:def 1
.= the carrier of X by A18, A29, FINSEQ_1:42 ;
for x1, x2 being Point of X holds h . (x1 + x2) = (h . x1) + (h . x2)

proof

let x1, x2 be Point of X; :: thesis:
consider g1 being Lipschitzian MultilinearOperator of Y,Z such that
A32: ( g1 = f . x1 & ( for py being Point of (product Y) holds (I . f) . (py ^ <*x1*>) = g1 . py ) ) by A12;
consider g2 being Lipschitzian MultilinearOperator of Y,Z such that
A33: ( g2 = f . x2 & ( for py being Point of (product Y) holds (I . f) . (py ^ <*x2*>) = g2 . py ) ) by A12;
consider g12 being Lipschitzian MultilinearOperator of Y,Z such that
A34: ( g12 = f . (x1 + x2) & ( for py being Point of (product Y) holds (I . f) . (py ^ <*(x1 + x2)*>) = g12 . py ) ) by A12;
A35: f1 is additive ;
A36: g12 = (f . x1) + (f . x2) by A34, A35;
A37: h . (x1 + x2) = (I . f) . ((reproj (i,z)) . (x1 + x2)) by FUNCT_1:13, A10, A31
.= (I . f) . (y ^ <*(x1 + x2)*>) by A14, A15, A18, A20, A28, Th33, XXREAL_0:1
.= ((f . x1) + (f . x2)) . y by A34, A36
.= (g1 . y) + (g2 . y) by A32, A33, LOPBAN10:48 ;
A38: h . x1 = (I . f) . ((reproj (i,z)) . x1) by FUNCT_1:13, A10, A31
.= (I . f) . (y ^ <*x1*>) by A14, A15, A18, A20, A28, Th33, XXREAL_0:1
.= g1 . y by A32 ;
h . x2 = (I . f) . ((reproj (i,z)) . x2) by A10, A31, FUNCT_1:13
.= (I . f) . (y ^ <*x2*>) by A14, A15, A18, A20, A28, Th33, XXREAL_0:1
.= g2 . y by A33 ;
hence h . (x1 + x2) = (h . x1) + (h . x2) by A37, A38; :: thesis:

end;

then A40: h is additive ;
for x0 being Point of X
for a being Real holds h . (a * x0) = a * (h . x0)

proof

let x0 be Point of X; :: thesis:
let a be Real; :: thesis:
consider g1 being Lipschitzian MultilinearOperator of Y,Z such that
A41: ( g1 = f . x0 & ( for py being Point of (product Y) holds (I . f) . (py ^ <*x0*>) = g1 . py ) ) by A12;
consider g2 being Lipschitzian MultilinearOperator of Y,Z such that
A42: ( g2 = f . (a * x0) & ( for py being Point of (product Y) holds (I . f) . (py ^ <*(a * x0)*>) = g2 . py ) ) by A12;
A43: g2 = a * (f1 . x0) by A42, LOPBAN_1:def 5;
A44: h . (a * x0) = (I . f) . ((reproj (i,z)) . (a * x0)) by A10, A31, FUNCT_1:13
.= (I . f) . (y ^ <*(a * x0)*>) by A14, A15, A18, A20, A28, Th33, XXREAL_0:1
.= (a * (f . x0)) . y by A42, A43
.= a * (g1 . y) by A41, LOPBAN10:49 ;
h . x0 = (I . f) . ((reproj (i,z)) . x0) by A10, A31, FUNCT_1:13
.= (I . f) . (y ^ <*x0*>) by A14, A15, A18, A20, A28, Th33, XXREAL_0:1
.= g1 . y by A41 ;
hence h . (a * x0) = a * (h . x0) by A44; :: thesis:

end;

hence Jf * (reproj (i,z)) is LinearOperator of ((Y ^ <*X*>) . i),Z by A30, A40, LOPBAN_1:def 5; :: thesis:

end;

then reconsider If = I . f as MultilinearOperator of (Y ^ <*X*>),Z by A10, LOPBAN10:def 6;
set K = ||.f.||;
A46: 0 <= ||.f.|| by LOPBAN_1:33;
A47: for z being Point of (product (Y ^ <*X*>)) holds ||.(If . z).|| <= ||.f.|| * (NrProduct z)

proof

let z be Element of (product (Y ^ <*X*>)); :: thesis:
consider py, px being FinSequence such that
A48: ( z = py ^ px & py in product (carr Y) & px in product <* the carrier of X*> ) by A6, RLAFFIN3:2;
reconsider py = py as Point of (product Y) by A3, A48;
consider x1 being Point of X such that
A49: px = <*x1*> by A2, A48, Th12;
consider cy being Function such that
A50: ( py = cy & dom cy = dom (carr Y) & ( for i being object st i in dom (carr Y) holds
cy . i in (carr Y) . i ) ) by A48, CARD_3:def 5;
reconsider cy = cy as FinSequence by A50;
consider g being Lipschitzian MultilinearOperator of Y,Z such that
A51: ( g = f . x1 & ( for p being Point of (product Y) holds (I . f) . (p ^ <*x1*>) = g . p ) ) by A12;
A52: (I . f) . z = g . py by A51, A48, A49;
A53: ||.(g . py).|| <= ||.(f . x1).|| * (NrProduct py) by A51, LOPBAN10:45;
A54: 0 <= NrProduct py by XXREAL_0:def 7;
||.(f1 . x1).|| <= ||.f.|| * ||.x1.|| by LOPBAN_1:32;
then A55: ||.(f . x1).|| * (NrProduct py) <= (||.f.|| * ||.x1.||) * (NrProduct py) by A54, XREAL_1:64;
||.x1.|| * (NrProduct py) = NrProduct z by A48, A49, Th35;
hence ||.(If . z).|| <= ||.f.|| * (NrProduct z) by A52, A53, A55, XXREAL_0:2; :: thesis:

end;

hence A56: I . f is Lipschitzian MultilinearOperator of (Y ^ <*X*>),Z by LOPBAN10:def 10, LOPBAN_1:33; :: thesis:
hence I . f in the carrier of (R_NormSpace_of_BoundedMultilinearOperators ((Y ^ <*X*>),Z)) by LOPBAN10:def 11; :: thesis:
reconsider If1 = I . f as Point of (R_NormSpace_of_BoundedMultilinearOperators ((Y ^ <*X*>),Z)) by A56, LOPBAN10:def 11;
reconsider If2 = I . f as Lipschitzian MultilinearOperator of (Y ^ <*X*>),Z by A47, LOPBAN10:def 10, LOPBAN_1:33;

now :: thesis:

let r be Real; :: thesis:
assume r in PreNorms If2 ; :: thesis:
then consider z being VECTOR of (product (Y ^ <*X*>)) such that
A57: ( r = ||.(If2 . z).|| & ( for i being Element of dom (Y ^ <*X*>) holds ||.(z . i).|| <= 1 ) ) ;
( 0 <= NrProduct z & NrProduct z <= 1 ) by A57, LOPBAN10:35;
then A58: ||.f.|| * (NrProduct z) <= ||.f.|| * 1 by A46, XREAL_1:64;
||.(If2 . z).|| <= ||.f.|| * (NrProduct z) by A47;
hence r <= ||.f.|| by A57, A58, XXREAL_0:2; :: thesis:

end;

then A59: upper_bound (PreNorms If2) <= ||.f.|| by SEQ_4:45;
A60: (BoundedMultilinearOperatorsNorm ((Y ^ <*X*>),Z)) . If2 = ||.If1.|| by NORMSP_0:def 1;
A61: ||.If1.|| <= ||.f.|| by A59, A60, LOPBAN10:43;
set SLYZ = R_NormSpace_of_BoundedMultilinearOperators (Y,Z);
reconsider f1 = f as Lipschitzian LinearOperator of X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)) by LOPBAN_1:def 9;

now :: thesis:

let r be Real; :: thesis:
assume r in PreNorms f1 ; :: thesis:
then consider x1 being VECTOR of X such that
A62: ( r = ||.(f1 . x1).|| & ||.x1.|| <= 1 ) ;
consider g being Lipschitzian MultilinearOperator of Y,Z such that
A63: ( g = f . x1 & ( for p being Point of (product Y) holds (I . f) . (p ^ <*x1*>) = g . p ) ) by A12;
A64: ( 0 <= ||.If1.|| & 0 <= ||.x1.|| ) by NORMSP_1:4;

now :: thesis:

let r be Real; :: thesis:
assume r in PreNorms g ; :: thesis:
then consider py being VECTOR of (product Y) such that
A65: ( r = ||.(g . py).|| & ( for i being Element of dom Y holds ||.(py . i).|| <= 1 ) ) ;
reconsider pz = py ^ <*x1*> as Point of (product (Y ^ <*X*>)) by Th34;
||.(g . py).|| = ||.(If2 . pz).|| by A63;
then A66: ||.(g . py).|| <= ||.If1.|| * (NrProduct pz) by LOPBAN10:45;
A67: ||.x1.|| * (NrProduct py) = NrProduct pz by Th35;
( 0 <= NrProduct py & NrProduct py <= 1 ) by A65, LOPBAN10:35;
then ||.x1.|| * (NrProduct py) <= ||.x1.|| * 1 by A64, XREAL_1:64;
then ||.If1.|| * (NrProduct pz) <= ||.If1.|| * ||.x1.|| by A64, A67, XREAL_1:64;
hence r <= ||.If1.|| * ||.x1.|| by A65, A66, XXREAL_0:2; :: thesis:

end;

then A68: upper_bound (PreNorms g) <= ||.If1.|| * ||.x1.|| by SEQ_4:45;
A69: (BoundedMultilinearOperatorsNorm (Y,Z)) . g = ||.(f . x1).|| by A63, NORMSP_0:def 1;
A70: ||.(f . x1).|| <= ||.If1.|| * ||.x1.|| by LOPBAN10:43, A68, A69;
||.If1.|| * ||.x1.|| <= ||.If1.|| * 1 by A62, A64, XREAL_1:64;
hence r <= ||.If1.|| by A62, A70, XXREAL_0:2; :: thesis:

end;

then A71: upper_bound (PreNorms f1) <= ||.If1.|| by SEQ_4:45;
A72: (BoundedLinearOperatorsNorm (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))) . f = ||.f.|| by NORMSP_0:def 1;
(BoundedLinearOperatorsNorm (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))) . f1 = upper_bound (PreNorms f1) by LOPBAN_1:30;
hence ex If being Point of (R_NormSpace_of_BoundedMultilinearOperators ((Y ^ <*X*>),Z)) st
( If = I . f & ||.f.|| = ||.If.|| ) by A61, A71, A72, XXREAL_0:1; :: thesis:

end;

then rng I c= the carrier of (R_NormSpace_of_BoundedMultilinearOperators ((Y ^ <*X*>),Z)) by FUNCT_2:114;
then reconsider I = I as Function of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))), the carrier of (R_NormSpace_of_BoundedMultilinearOperators ((Y ^ <*X*>),Z)) by FUNCT_2:6;
A73: for f1, f2 being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))) holds I . (f1 + f2) = (I . f1) + (I . f2)

proof

let f1, f2 be Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))); :: thesis:
for z being Point of (product (Y ^ <*X*>)) holds (I . (f1 + f2)) . z = ((I . f1) . z) + ((I . f2) . z)

proof

let z be Point of (product (Y ^ <*X*>)); :: thesis:
consider py, px being FinSequence such that
A74: ( z = py ^ px & py in product (carr Y) & px in product <* the carrier of X*> ) by A6, RLAFFIN3:2;
reconsider py = py as Point of (product Y) by A3, A74;
consider x1 being Point of X such that
A75: px = <*x1*> by A2, A74, Th12;
consider g1 being Lipschitzian MultilinearOperator of Y,Z such that
A76: ( g1 = f1 . x1 & ( for p being Point of (product Y) holds (I . f1) . (p ^ <*x1*>) = g1 . p ) ) by A9;
consider g2 being Lipschitzian MultilinearOperator of Y,Z such that
A77: ( g2 = f2 . x1 & ( for ppy being Point of (product Y) holds (I . f2) . (ppy ^ <*x1*>) = g2 . ppy ) ) by A9;
consider g12 being Lipschitzian MultilinearOperator of Y,Z such that
A78: ( g12 = (f1 + f2) . x1 & ( for p being Point of (product Y) holds (I . (f1 + f2)) . (p ^ <*x1*>) = g12 . p ) ) by A9;
A79: (I . f2) . z = g2 . py by A74, A75, A77;
A80: (I . (f1 + f2)) . z = g12 . py by A74, A75, A78;
((f1 . x1) . py) + ((f2 . x1) . py) = ((f1 . x1) + (f2 . x1)) . py by LOPBAN10:48
.= g12 . py by A78, LOPBAN_1:35 ;
hence (I . (f1 + f2)) . z = ((I . f1) . z) + ((I . f2) . z) by A74, A75, A76, A77, A79, A80; :: thesis:

end;

hence I . (f1 + f2) = (I . f1) + (I . f2) by LOPBAN10:48; :: thesis:

end;

for f1 being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z))))
for a being Real holds I . (a * f1) = a * (I . f1)

proof

let f1 be Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))); :: thesis:
let a be Real; :: thesis:
for z being Point of (product (Y ^ <*X*>)) holds (I . (a * f1)) . z = a * ((I . f1) . z)

proof

let z be Point of (product (Y ^ <*X*>)); :: thesis:
consider py, px being FinSequence such that
A82: ( z = py ^ px & py in product (carr Y) & px in product <* the carrier of X*> ) by A6, RLAFFIN3:2;
reconsider py = py as Point of (product Y) by A3, A82;
consider ppx being Point of X such that
A83: px = <*ppx*> by A2, A82, Th12;
consider g1 being Lipschitzian MultilinearOperator of Y,Z such that
A84: ( g1 = f1 . ppx & ( for p being Point of (product Y) holds (I . f1) . (p ^ <*ppx*>) = g1 . p ) ) by A9;
consider g2 being Lipschitzian MultilinearOperator of Y,Z such that
A85: ( g2 = (a * f1) . ppx & ( for p being Point of (product Y) holds (I . (a * f1)) . (p ^ <*ppx*>) = g2 . p ) ) by A9;
A86: (I . (a * f1)) . z = g2 . py by A82, A83, A85;
a * ((f1 . ppx) . py) = (a * (f1 . ppx)) . py by LOPBAN10:49
.= g2 . py by A85, LOPBAN_1:36 ;
hence (I . (a * f1)) . z = a * ((I . f1) . z) by A82, A83, A84, A86; :: thesis:

end;

hence I . (a * f1) = a * (I . f1) by LOPBAN10:49; :: thesis:

end;

then reconsider I = I as LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))),(R_NormSpace_of_BoundedMultilinearOperators ((Y ^ <*X*>),Z)) by A73, LOPBAN_1:def 5, VECTSP_1:def 20;
A88: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))) holds
( ||.u.|| = ||.(I . u).|| & ( for y being Point of (product Y)
for x being Point of X holds (I . u) . (y ^ <*x*>) = (u . x) . y ) )

proof

let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))); :: thesis:
ex Iu being Point of (R_NormSpace_of_BoundedMultilinearOperators ((Y ^ <*X*>),Z)) st
( Iu = I . u & ||.u.|| = ||.Iu.|| ) by A9;
hence ||.u.|| = ||.(I . u).|| ; :: thesis:
let y be Point of (product Y); :: thesis:
let x be Point of X; :: thesis:
ex G being Lipschitzian MultilinearOperator of Y,Z st
( G = u . x & ( for y being Point of (product Y) holds (I . u) . (y ^ <*x*>) = G . y ) ) by A9;
hence (I . u) . (y ^ <*x*>) = (u . x) . y ; :: thesis:

end;

A89: for If being object st If in the carrier of (R_NormSpace_of_BoundedMultilinearOperators ((Y ^ <*X*>),Z)) holds
ex f being object st
( f in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))) & If = I . f )

proof

let If be object ; :: thesis:
assume A90: If in the carrier of (R_NormSpace_of_BoundedMultilinearOperators ((Y ^ <*X*>),Z)) ; :: thesis:
then reconsider Iu = If as Lipschitzian MultilinearOperator of (Y ^ <*X*>),Z by LOPBAN10:def 11;
reconsider Lu = If as Point of (R_NormSpace_of_BoundedMultilinearOperators ((Y ^ <*X*>),Z)) by A90;
defpred S₁[ object , object ] means ex x1 being Point of X ex g being Lipschitzian MultilinearOperator of Y,Z st
( $1 = x1 & $2 = g & ( for py being Point of (product Y) holds Iu . (py ^ <*x1*>) = g . py ) );
set LYZ = the carrier of (R_NormSpace_of_BoundedMultilinearOperators (Y,Z));
A91: for v being Element of the carrier of X ex w being Element of the carrier of (R_NormSpace_of_BoundedMultilinearOperators (Y,Z)) st S₁[v,w]

proof

let x1 be Element of the carrier of X; :: thesis:
defpred S₂[ object , object ] means ex py being Point of (product Y) st
( $1 = py & $2 = Iu . (py ^ <*x1*>) );
A92: for v being Element of the carrier of (product Y) ex w being Element of the carrier of Z st S₂[v,w]

proof

let v be Element of the carrier of (product Y); :: thesis:
reconsider If = v ^ <*x1*> as Point of (product (Y ^ <*X*>)) by Th34;
Iu . If is Point of Z ;
hence ex w being Element of the carrier of Z st S₂[v,w] ; :: thesis:

end;

consider g1 being Function of the carrier of (product Y), the carrier of Z such that
A93: for py being Element of the carrier of (product Y) holds S₂[py,g1 . py] from FUNCT_2:sch 3(A92);
for i being Element of dom Y
for py being Element of (product Y) holds g1 * (reproj (i,py)) is LinearOperator of (Y . i),Z

proof

let i be Element of dom Y; :: thesis:
let py be Element of (product Y); :: thesis:
consider cy being Function such that
A94: ( py = cy & dom cy = dom (carr Y) & ( for i being object st i in dom (carr Y) holds
cy . i in (carr Y) . i ) ) by A3, CARD_3:def 5;
reconsider cy = cy as FinSequence by A94;
A95: dom (Y ^ <*X*>) = Seg (len (Y ^ <*X*>)) by FINSEQ_1:def 3
.= Seg ((len Y) + (len <*X*>)) by FINSEQ_1:22
.= Seg ((len Y) + 1) by FINSEQ_1:40 ;
i in dom Y ;
then i in Seg (len Y) by FINSEQ_1:def 3;
then A96: ( 1 <= i & i <= len Y ) by FINSEQ_1:1;
len Y <= (len Y) + 1 by NAT_1:11;
then i <= (len Y) + 1 by XXREAL_0:2, A96;
then i in Seg ((len Y) + 1) by A96;
then reconsider i0 = i as Element of dom (Y ^ <*X*>) by A95;
reconsider z = py ^ <*x1*> as Point of (product (Y ^ <*X*>)) by Th34;
A97: (Y ^ <*X*>) . i0 = Y . i by FINSEQ_1:def 7;
reconsider L = g1 * (reproj (i,py)) as Function of (Y . i),Z ;
A98: dom (reproj (i0,z)) = the carrier of ((Y ^ <*X*>) . i0) by FUNCT_2:def 1
.= the carrier of (Y . i) by FINSEQ_1:def 7 ;
dom Iu = the carrier of (product (Y ^ <*X*>)) by FUNCT_2:def 1;
then rng (reproj (i0,z)) c= dom Iu ;
then A99: dom (Iu * (reproj (i0,z))) = the carrier of (Y . i) by A98, RELAT_1:27;
for t being object st t in dom (Iu * (reproj (i0,z))) holds
(Iu * (reproj (i0,z))) . t = (g1 * (reproj (i,py))) . t

proof

let t be object ; :: thesis:
assume A100: t in dom (Iu * (reproj (i0,z))) ; :: thesis:
then reconsider t1 = t as Point of ((Y ^ <*X*>) . i0) ;
reconsider t2 = t as Point of (Y . i) by A100, FINSEQ_1:def 7;
A101: S₂[(reproj (i,py)) . t2,g1 . ((reproj (i,py)) . t2)] by A93;
thus (Iu * (reproj (i0,z))) . t = Iu . ((reproj (i0,z)) . t1) by FUNCT_2:15
.= g1 . ((reproj (i,py)) . t2) by A101, Th32
.= (g1 * (reproj (i,py))) . t by FUNCT_2:15 ; :: thesis:

end;

then Iu * (reproj (i0,z)) = g1 * (reproj (i,py)) by A97, A99;
hence g1 * (reproj (i,py)) is LinearOperator of (Y . i),Z by A97, LOPBAN10:def 6; :: thesis:

end;

then reconsider g1 = g1 as MultilinearOperator of Y,Z by LOPBAN10:def 6;
set K = ||.x1.|| * ||.Lu.||;
A102: ( 0 <= ||.Lu.|| & 0 <= ||.x1.|| ) by NORMSP_1:4;
for py being Point of (product Y) holds ||.(g1 . py).|| <= (||.x1.|| * ||.Lu.||) * (NrProduct py)

proof

let py be Element of (product Y); :: thesis:
consider cy being Function such that
A103: ( py = cy & dom cy = dom (carr Y) & ( for i being object st i in dom (carr Y) holds
cy . i in (carr Y) . i ) ) by A3, CARD_3:def 5;
reconsider cy = cy as FinSequence by A103;
reconsider z = py ^ <*x1*> as Point of (product (Y ^ <*X*>)) by Th34;
A104: S₂[py,g1 . py] by A93;
A105: ||.(Iu . z).|| <= ||.Lu.|| * (NrProduct z) by LOPBAN10:45;
||.x1.|| * (NrProduct py) = NrProduct z by Th35;
hence ||.(g1 . py).|| <= (||.x1.|| * ||.Lu.||) * (NrProduct py) by A104, A105; :: thesis:

end;

then reconsider g1 = g1 as Lipschitzian MultilinearOperator of Y,Z by A102, LOPBAN10:def 10, XREAL_1:127;
reconsider g2 = g1 as Element of the carrier of (R_NormSpace_of_BoundedMultilinearOperators (Y,Z)) by LOPBAN10:def 11;
take g2 ; :: thesis:
for py being Point of (product Y) holds Iu . (py ^ <*x1*>) = g1 . py

proof

let py be Point of (product Y); :: thesis:
S₂[py,g1 . py] by A93;
hence Iu . (py ^ <*x1*>) = g1 . py ; :: thesis:

end;

hence S₁[x1,g2] ; :: thesis:

end;

consider f0 being Function of the carrier of X, the carrier of (R_NormSpace_of_BoundedMultilinearOperators (Y,Z)) such that
A106: for x being Element of the carrier of X holds S₁[x,f0 . x] from FUNCT_2:sch 3(A91);
A107: for x0 being Point of X
for y0 being Point of (product Y) holds Iu . (y0 ^ <*x0*>) = (f0 . x0) . y0

proof

let x0 be Point of X; :: thesis:
ex x1 being Point of X ex g being Lipschitzian MultilinearOperator of Y,Z st
( x1 = x0 & f0 . x0 = g & ( for py being Point of (product Y) holds Iu . (py ^ <*x1*>) = g . py ) ) by A106;
hence for py being Point of (product Y) holds Iu . (py ^ <*x0*>) = (f0 . x0) . py ; :: thesis:

end;

for x1, x2 being Point of X holds f0 . (x1 + x2) = (f0 . x1) + (f0 . x2)

proof

let x1, x2 be Point of X; :: thesis:
for py being Point of (product Y) holds (f0 . (x1 + x2)) . py = ((f0 . x1) . py) + ((f0 . x2) . py)

proof

let py be Point of (product Y); :: thesis:
consider cy being Function such that
A108: ( py = cy & dom cy = dom (carr Y) & ( for i being object st i in dom (carr Y) holds
cy . i in (carr Y) . i ) ) by A3, CARD_3:def 5;
A109: dom cy = Seg (len (carr Y)) by A108, FINSEQ_1:def 3;
reconsider cy = cy as FinSequence by A108;
A110: len py = len (carr Y) by A108, A109, FINSEQ_1:def 3
.= len Y by PRVECT_1:def 11 ;
A111: Iu . (py ^ <*x1*>) = (f0 . x1) . py by A107;
A112: Iu . (py ^ <*x2*>) = (f0 . x2) . py by A107;
A113: Iu . (py ^ <*(x1 + x2)*>) = (f0 . (x1 + x2)) . py by A107;
A114: len (Y ^ <*X*>) = (len Y) + (len <*X*>) by FINSEQ_1:22
.= (len Y) + 1 by FINSEQ_1:40 ;
reconsider z1 = py ^ <*x1*> as Point of (product (Y ^ <*X*>)) by Th34;
reconsider z2 = py ^ <*x2*> as Point of (product (Y ^ <*X*>)) by Th34;
reconsider z12 = py ^ <*(x1 + x2)*> as Point of (product (Y ^ <*X*>)) by Th34;
(len Y) + 1 in Seg ((len Y) + 1) by FINSEQ_1:4;
then reconsider j = (len py) + 1 as Element of dom (Y ^ <*X*>) by A110, A114, FINSEQ_1:def 3;
A115: (Y ^ <*X*>) . j = X by A110, FINSEQ_1:42;
A116: Iu . (py ^ <*x1*>) = Iu . ((reproj (j,z1)) . x1) by Th33
.= (Iu * (reproj (j,z1))) . x1 by A115, FUNCT_2:15 ;
A117: Iu . (py ^ <*x2*>) = Iu . ((reproj (j,z1)) . x2) by Th33
.= (Iu * (reproj (j,z1))) . x2 by A115, FUNCT_2:15 ;
A118: Iu . (py ^ <*(x1 + x2)*>) = Iu . ((reproj (j,z1)) . (x1 + x2)) by Th33
.= (Iu * (reproj (j,z1))) . (x1 + x2) by A115, FUNCT_2:15 ;
reconsider L = Iu * (reproj (j,z1)) as LinearOperator of X,Z by A115, LOPBAN10:def 6;
L is additive ;
hence (f0 . (x1 + x2)) . py = ((f0 . x1) . py) + ((f0 . x2) . py) by A116, A117, A118, A111, A112, A113; :: thesis:

end;

hence f0 . (x1 + x2) = (f0 . x1) + (f0 . x2) by LOPBAN10:48; :: thesis:

end;

then A119: f0 is additive ;
for x1 being Point of X
for a being Real holds f0 . (a * x1) = a * (f0 . x1)

proof

let x1 be Point of X; :: thesis:
let a be Real; :: thesis:
for py being Point of (product Y) holds (f0 . (a * x1)) . py = a * ((f0 . x1) . py)

proof

let py be Point of (product Y); :: thesis:
consider cy being Function such that
A120: ( py = cy & dom cy = dom (carr Y) & ( for i being object st i in dom (carr Y) holds
cy . i in (carr Y) . i ) ) by A3, CARD_3:def 5;
A121: dom cy = Seg (len (carr Y)) by A120, FINSEQ_1:def 3;
reconsider cy = cy as FinSequence by A120;
A122: len py = len (carr Y) by A120, A121, FINSEQ_1:def 3
.= len Y by PRVECT_1:def 11 ;
A123: Iu . (py ^ <*(a * x1)*>) = (f0 . (a * x1)) . py by A107;
A124: len (Y ^ <*X*>) = (len Y) + (len <*X*>) by FINSEQ_1:22
.= (len Y) + 1 by FINSEQ_1:40 ;
reconsider z1 = py ^ <*x1*> as Point of (product (Y ^ <*X*>)) by Th34;
reconsider z2 = py ^ <*(a * x1)*> as Point of (product (Y ^ <*X*>)) by Th34;
(len Y) + 1 in Seg ((len Y) + 1) by FINSEQ_1:4;
then reconsider j = (len py) + 1 as Element of dom (Y ^ <*X*>) by A122, A124, FINSEQ_1:def 3;
A125: (Y ^ <*X*>) . j = X by A122, FINSEQ_1:42;
A126: Iu . (py ^ <*x1*>) = Iu . ((reproj (j,z1)) . x1) by Th33
.= (Iu * (reproj (j,z1))) . x1 by A125, FUNCT_2:15 ;
A127: Iu . (py ^ <*(a * x1)*>) = Iu . ((reproj (j,z1)) . (a * x1)) by Th33
.= (Iu * (reproj (j,z1))) . (a * x1) by A125, FUNCT_2:15 ;
reconsider L = Iu * (reproj (j,z1)) as LinearOperator of X,Z by A125, LOPBAN10:def 6;
L . (a * x1) = a * (L . x1) by LOPBAN_1:def 5;
hence (f0 . (a * x1)) . py = a * ((f0 . x1) . py) by A107, A123, A126, A127; :: thesis:

end;

hence f0 . (a * x1) = a * (f0 . x1) by LOPBAN10:49; :: thesis:

end;

then reconsider f0 = f0 as LinearOperator of X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)) by A119, LOPBAN_1:def 5;
consider K being Real such that
A128: ( 0 <= K & ( for z1 being Point of (product (Y ^ <*X*>)) holds ||.(Iu . z1).|| <= K * (NrProduct z1) ) ) by LOPBAN10:def 10;
for x1 being Point of X holds ||.(f0 . x1).|| <= K * ||.x1.||

proof

let x1 be Point of X; :: thesis:
reconsider fx1 = f0 . x1 as Lipschitzian MultilinearOperator of Y,Z by LOPBAN10:def 11;
reconsider fx2 = f0 . x1 as Point of (R_NormSpace_of_BoundedMultilinearOperators (Y,Z)) ;
0 <= ||.x1.|| by NORMSP_1:4;
then A129: 0 <= K * ||.x1.|| by XREAL_1:127, A128;
A130: for px being Point of (product Y) holds ||.(fx1 . px).|| <= (K * ||.x1.||) * (NrProduct px)

proof

let py be Point of (product Y); :: thesis:
consider cy being Function such that
A131: ( py = cy & dom cy = dom (carr Y) & ( for i being object st i in dom (carr Y) holds
cy . i in (carr Y) . i ) ) by A3, CARD_3:def 5;
reconsider cy = cy as FinSequence by A131;
reconsider z1 = py ^ <*x1*> as Point of (product (Y ^ <*X*>)) by Th34;
A132: ||.(Iu . z1).|| <= K * (NrProduct z1) by A128;
||.x1.|| * (NrProduct py) = NrProduct z1 by Th35;
hence ||.(fx1 . py).|| <= (K * ||.x1.||) * (NrProduct py) by A107, A132; :: thesis:

end;

now :: thesis:

let r be Real; :: thesis:
assume r in PreNorms fx1 ; :: thesis:
then consider py being VECTOR of (product Y) such that
A133: ( r = ||.(fx1 . py).|| & ( for i being Element of dom Y holds ||.(py . i).|| <= 1 ) ) ;
( 0 <= NrProduct py & NrProduct py <= 1 ) by A133, LOPBAN10:35;
then A134: (K * ||.x1.||) * (NrProduct py) <= (K * ||.x1.||) * 1 by A129, XREAL_1:64;
||.(fx1 . py).|| <= (K * ||.x1.||) * (NrProduct py) by A130;
hence r <= K * ||.x1.|| by A133, A134, XXREAL_0:2; :: thesis:

end;

then A135: upper_bound (PreNorms fx1) <= K * ||.x1.|| by SEQ_4:45;
(BoundedMultilinearOperatorsNorm (Y,Z)) . fx1 = ||.(f0 . x1).|| by NORMSP_0:def 1;
hence ||.(f0 . x1).|| <= K * ||.x1.|| by A135, LOPBAN10:43; :: thesis:

end;

then reconsider f0 = f0 as Lipschitzian LinearOperator of X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)) by A128, LOPBAN_1:def 8;
take f0 ; :: thesis:
thus f0 in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))) by LOPBAN_1:def 9; :: thesis:
reconsider f = f0 as Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))) by LOPBAN_1:def 9;
reconsider L = I . f as Lipschitzian MultilinearOperator of (Y ^ <*X*>),Z by LOPBAN10:def 11;
for z being Element of (product (Y ^ <*X*>)) holds L . z = Iu . z

proof

let z be Point of (product (Y ^ <*X*>)); :: thesis:
consider py, px being FinSequence such that
A136: ( z = py ^ px & py in product (carr Y) & px in product <* the carrier of X*> ) by A6, RLAFFIN3:2;
reconsider py = py as Point of (product Y) by A3, A136;
consider x1 being Point of X such that
A137: px = <*x1*> by A2, A136, Th12;
consider x2 being Point of X, g1 being Lipschitzian MultilinearOperator of Y,Z such that
A138: ( x1 = x2 & f0 . x1 = g1 & ( for py being Point of (product Y) holds Iu . (py ^ <*x2*>) = g1 . py ) ) by A106;
A139: Iu . z = g1 . py by A136, A137, A138;
consider g being Lipschitzian MultilinearOperator of Y,Z such that
A140: ( g = f . x1 & ( for py being Point of (product Y) holds (I . f) . (py ^ <*x1*>) = g . py ) ) by A9;
thus L . z = Iu . z by A136, A137, A138, A139, A140; :: thesis:

end;

then L = Iu ;
hence If = I . f0 ; :: thesis:

end;

for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))) holds ||.(I . u).|| <= 1 * ||.u.|| by A88;
then reconsider I = I as Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))),(R_NormSpace_of_BoundedMultilinearOperators ((Y ^ <*X*>),Z)) by LOPBAN_1:def 8;
take I ; :: thesis:
thus ( I is one-to-one & I is onto ) by A1, A89, FUNCT_1:52, FUNCT_2:10; :: thesis:
thus ( I is isometric & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))) holds
( ||.u.|| = ||.(I . u).|| & ( for y being Point of (product Y)
for x being Point of X holds (I . u) . (y ^ <*x*>) = (u . x) . y ) ) ) ) by A88, NDIFF_7:7; :: thesis: