let Y be RealNormSpace; :: thesis:
defpred S₁[ Nat] means for X being RealNormSpace-Sequence st $1 = len X & 1 <= len X holds
ex I being Lipschitzian LinearOperator of (NestingLB (X,Y)),(R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st
( I is one-to-one & I is onto & I is isometric & ( for u being Point of (NestingLB (X,Y))
for x being Point of (product X) ex g being FinSequence st
( len g = len X & g . 1 = u & ( for i being Element of NAT st 1 <= i & i < len X holds
ex Xi being RealNormSpace-Sequence ex h being Point of (NestingLB (Xi,Y)) st
( Xi = X | (((len X) -' i) + 1) & h = g . i & g . (i + 1) = h . (x . (((len X) -' i) + 1)) ) ) & ex X1 being RealNormSpace-Sequence ex h being Point of (NestingLB (X1,Y)) st
( X1 = <*(X . 1)*> & h = g . (len X) & (I . u) . x = h . (x . 1) ) ) ) );
A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A3: for X being RealNormSpace-Sequence st n = len X & 1 <= len X holds
ex I being Lipschitzian LinearOperator of (NestingLB (X,Y)),(R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st
( I is one-to-one & I is onto & I is isometric & ( for u being Point of (NestingLB (X,Y))
for x being Point of (product X) ex g being FinSequence st
( len g = len X & g . 1 = u & ( for i being Element of NAT st 1 <= i & i < len X holds
ex Xi being RealNormSpace-Sequence ex h being Point of (NestingLB (Xi,Y)) st
( Xi = X | (((len X) -' i) + 1) & h = g . i & g . (i + 1) = h . (x . (((len X) -' i) + 1)) ) ) & ex X1 being RealNormSpace-Sequence ex h being Point of (NestingLB (X1,Y)) st
( X1 = <*(X . 1)*> & h = g . (len X) & (I . u) . x = h . (x . 1) ) ) ) ) ; :: thesis:
let X be RealNormSpace-Sequence; :: thesis:
assume A4: ( n + 1 = len X & 1 <= len X ) ; :: thesis:
set K = X | n;
A5: X = (X | n) ^ <*(X . (n + 1))*> by A4, FINSEQ_3:55;
A6: len (X | n) = n by A4, FINSEQ_3:53;

per cases ;

suppose A7: n = 0 ; :: thesis:

1 in Seg (len X) by A4;
then 1 in dom X by FINSEQ_1:def 3;
then X . 1 in rng X by FUNCT_1:3;
then reconsider X1 = X . 1 as RealNormSpace by PRVECT_2:def 10;
A8: X = <*X1*> by A4, A7, FINSEQ_1:40;
consider f being Function such that
A9: ( dom f = NAT & NestingLB (X,Y) = f . (len X) & f . 0 = Y & ( for j being Nat st j < len X holds
ex V being RealNormSpace ex k being Element of dom X st
( V = f . j & j + 1 = k & f . (j + 1) = R_NormSpace_of_BoundedLinearOperators ((X . k),V) ) ) ) by Def3;
consider V being RealNormSpace, k being Element of dom X such that
A10: ( V = f . 0 & 0 + 1 = k & f . (0 + 1) = R_NormSpace_of_BoundedLinearOperators ((X . k),V) ) by A4, A7, A9;
consider I being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X1,Y)),(R_NormSpace_of_BoundedLinearOperators ((product <*X1*>),Y)) such that
A12: ( I is one-to-one & I is onto & I is isometric & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X1,Y))
for x1 being Point of X1 holds (I . u) . <*x1*> = u . x1 ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X1,Y)) holds ||.u.|| = ||.(I . u).|| ) ) by Th39;
A13: R_NormSpace_of_BoundedLinearOperators ((product <*X1*>),Y) = R_NormSpace_of_BoundedMultilinearOperators (<*X1*>,Y) by Th26;
reconsider I = I as Lipschitzian LinearOperator of (NestingLB (X,Y)),(R_NormSpace_of_BoundedMultilinearOperators (X,Y)) by A4, A7, A8, A9, A10, A13;
take I ; :: thesis:
thus ( I is one-to-one & I is onto & I is isometric ) by A4, A7, A8, A9, A10, A12, A13; :: thesis:
thus for u being Point of (NestingLB (X,Y))
for x being Point of (product X) ex g being FinSequence st
( len g = len X & g . 1 = u & ( for i being Element of NAT st 1 <= i & i < len X holds
ex Xi being RealNormSpace-Sequence ex h being Point of (NestingLB (Xi,Y)) st
( Xi = X | (((len X) -' i) + 1) & h = g . i & g . (i + 1) = h . (x . (((len X) -' i) + 1)) ) ) & ex X1 being RealNormSpace-Sequence ex h being Point of (NestingLB (X1,Y)) st
( X1 = <*(X . 1)*> & h = g . (len X) & (I . u) . x = h . (x . 1) ) ) :: thesis:

proof

let u be Point of (NestingLB (X,Y)); :: thesis:
let x be Point of (product X); :: thesis:
set g = <*u*>;
take <*u*> ; :: thesis:
thus len <*u*> = len X by FINSEQ_1:40, A7, A4; :: thesis:
thus <*u*> . 1 = u ; :: thesis:
thus for i being Element of NAT st 1 <= i & i < len X holds
ex Xi being RealNormSpace-Sequence ex h being Point of (NestingLB (Xi,Y)) st
( Xi = X | (((len X) -' i) + 1) & h = <*u*> . i & <*u*> . (i + 1) = h . (x . (((len X) -' i) + 1)) ) by A4, A7; :: thesis:
reconsider XX1 = <*(X . 1)*> as RealNormSpace-Sequence by A4, A7, FINSEQ_1:40;
reconsider h = u as Point of (NestingLB (XX1,Y)) by A4, A7, FINSEQ_1:40;
take XX1 ; :: thesis:
take h ; :: thesis:
thus ( XX1 = <*(X . 1)*> & h = <*u*> . (len X) ) by A4, A7; :: thesis:
consider x1 being Point of X1 such that
A14: x = <*x1*> by A8, Th12;
thus (I . u) . x = u . x1 by A4, A7, A9, A10, A12, A14
.= h . (x . 1) by A14 ; :: thesis:

end;

suppose A15: n <> 0 ; :: thesis:

then A16: 1 <= n by NAT_1:14;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then reconsider n1 = n + 1 as Element of dom X by A4, FINSEQ_1:def 3;
reconsider Xn1 = X . n1 as RealNormSpace ;
for x being set st x in rng (X | n) holds
x is RealNormSpace

proof

let x be set ; :: thesis:
assume x in rng (X | n) ; :: thesis:
then x in rng X by RELAT_1:70, TARSKI:def 3;
hence x is RealNormSpace by PRVECT_2:def 10; :: thesis:

end;

proof

let v be Element of (R_NormSpace_of_BoundedLinearOperators ((X . n1),(NestingLB (K,Y)))); :: thesis:
thus ||.(I . v).|| = ||.(I2 . (I1 . v)).|| by FUNCT_2:15
.= ||.(I1 . v).|| by A23
.= ||.v.|| by A22, NDIFF_7:7 ; :: thesis:

end;

then I is isometric by NDIFF_7:7;
then reconsider I = I as Lipschitzian LinearOperator of (NestingLB (X,Y)),(R_NormSpace_of_BoundedMultilinearOperators (X,Y)) by A20, A5;
take I ; :: thesis:
thus ( I is one-to-one & I is onto & I is isometric ) by A5, A20, A22, A23, A24, FUNCT_2:27, NDIFF_7:7; :: thesis:
thus for u being Point of (NestingLB (X,Y))
for x being Point of (product X) ex g being FinSequence st
( len g = len X & g . 1 = u & ( for i being Element of NAT st 1 <= i & i < len X holds
ex Xi being RealNormSpace-Sequence ex h being Point of (NestingLB (Xi,Y)) st
( Xi = X | (((len X) -' i) + 1) & h = g . i & g . (i + 1) = h . (x . (((len X) -' i) + 1)) ) ) & ex X1 being RealNormSpace-Sequence ex h being Point of (NestingLB (X1,Y)) st
( X1 = <*(X . 1)*> & h = g . (len X) & (I . u) . x = h . (x . 1) ) ) :: thesis:

proof

let u be Point of (NestingLB (X,Y)); :: thesis:
let x be Point of (product X); :: thesis:
consider pk, pxn1 being FinSequence such that
A25: ( x = pk ^ pxn1 & pk in product (carr K) & pxn1 in product <* the carrier of Xn1*> ) by A5, A19, RLAFFIN3:2;
reconsider pk = pk as Point of (product K) by A18, A25;
consider y being Point of Xn1 such that
A26: pxn1 = <*y*> by A17, A25, Th12;
ex g being Function st
( pk = g & dom g = dom (carr K) & ( for i being object st i in dom (carr K) holds
g . i in (carr K) . i ) ) by A18, CARD_3:def 5;
then dom pk = Seg (len (carr K)) by FINSEQ_1:def 3;
then A27: len pk = len (carr K) by FINSEQ_1:def 3
.= len K by PRVECT_1:def 11
.= n by A4, FINSEQ_3:53 ;
reconsider xn1 = x . (n + 1) as Point of Xn1 by A25, A26, A27, FINSEQ_1:42;
reconsider u1 = u as Lipschitzian LinearOperator of Xn1,(NestingLB (K,Y)) by A20, LOPBAN_1:def 9;
reconsider uxn1 = u1 . xn1 as Point of (NestingLB (K,Y)) ;
consider g1 being FinSequence such that
A28: ( len g1 = len K & g1 . 1 = uxn1 & ( for i being Element of NAT st 1 <= i & i < len K holds
ex Ki being RealNormSpace-Sequence ex h1 being Point of (NestingLB (Ki,Y)) st
( Ki = K | (((len K) -' i) + 1) & h1 = g1 . i & g1 . (i + 1) = h1 . (pk . (((len K) -' i) + 1)) ) ) & ex K1 being RealNormSpace-Sequence ex h1 being Point of (NestingLB (K1,Y)) st
( K1 = <*(K . 1)*> & h1 = g1 . (len K) & (I0 . uxn1) . pk = h1 . (pk . 1) ) ) by A21;
set g = <*u*> ^ g1;
take <*u*> ^ g1 ; :: thesis:
thus len (<*u*> ^ g1) = (len <*u*>) + (len g1) by FINSEQ_1:22
.= 1 + (len g1) by FINSEQ_1:40
.= len X by A4, A28, FINSEQ_3:53 ; :: thesis:
thus A29: (<*u*> ^ g1) . 1 = u by FINSEQ_1:41; :: thesis:
thus for i being Element of NAT st 1 <= i & i < len X holds
ex Xi being RealNormSpace-Sequence ex h being Point of (NestingLB (Xi,Y)) st
( Xi = X | (((len X) -' i) + 1) & h = (<*u*> ^ g1) . i & (<*u*> ^ g1) . (i + 1) = h . (x . (((len X) -' i) + 1)) ) :: thesis:

proof

let i be Element of NAT ; :: thesis:
assume A30: ( 1 <= i & i < len X ) ; :: thesis:
A31: i <= n by A30, A4, NAT_1:13;
A32: i -' 1 = i - 1 by A30, XREAL_1:48, XREAL_0:def 2;

per cases ;

suppose A33: 2 <= i ; :: thesis:

then A34: 2 - 1 <= i - 1 by XREAL_1:13;
then A35: 1 <= i -' 1 by A30, XREAL_1:48, XREAL_0:def 2;
i - 1 < i - 0 by XREAL_1:15;
then A36: i -' 1 < len K by A31, A6, A32, XXREAL_0:2;
then consider Xi being RealNormSpace-Sequence, h being Point of (NestingLB (Xi,Y)) such that
A37: ( Xi = K | (((len K) -' (i -' 1)) + 1) & h = g1 . (i -' 1) & g1 . ((i -' 1) + 1) = h . (pk . (((len K) -' (i -' 1)) + 1)) ) by A28, A35;
take Xi ; :: thesis:
take h ; :: thesis:
A39: ((len K) -' (i -' 1)) + 1 = ((len K) - (i - 1)) + 1 by A32, A36, XREAL_1:48, XREAL_0:def 2
.= (((len K) + 1) - i) + 1
.= ((len X) - i) + 1 by A4, FINSEQ_3:53
.= ((len X) -' i) + 1 by A30, XREAL_1:48, XREAL_0:def 2 ;
(len K) - (i -' 1) <= (len K) - 1 by A35, XREAL_1:13;
then ((len K) - (i -' 1)) + 1 <= ((len K) - 1) + 1 by XREAL_1:7;
then A40: ((len K) - (i -' 1)) + 1 <= n by A4, FINSEQ_3:53;
A41: ((len K) -' (i -' 1)) + 1 = ((len K) - (i -' 1)) + 1 by A36, XREAL_1:48, XREAL_0:def 2;
A43: len <*u*> = 1 by FINSEQ_1:40;
A44: (len <*u*>) + 1 = 1 + 1 by FINSEQ_1:40;
i <= i + 1 by NAT_1:11;
then A45: (len <*u*>) + 1 <= i + 1 by A33, A44, XXREAL_0:2;
A46: i + 1 <= (len g1) + 1 by A4, A6, A28, A30, NAT_1:13;
A47: ((len X) -' i) + 1 = ((len X) - i) + 1 by A30, XREAL_1:48, XREAL_0:def 2
.= (n - (i - 1)) + 1 by A4 ;
n - (i - 1) <= n - 1 by A34, XREAL_1:13;
then A48: (n - (i - 1)) + 1 <= (n - 1) + 1 by XREAL_1:7;
i - 1 < i - 0 by XREAL_1:15;
then A49: n - i < n - (i - 1) by XREAL_1:15;
0 <= n - i by A31, XREAL_1:48;
then 0 < n - (i - 1) by A49, XXREAL_0:2;
then 0 + 1 <= (n - (i - 1)) + 1 by XREAL_1:8;
then ((len X) -' i) + 1 in Seg n by A47, A48;
then A50: ((len X) -' i) + 1 in dom pk by A27, FINSEQ_1:def 3;
A51: g1 . (i -' 1) = g1 . (i - 1) by A30, XREAL_1:48, XREAL_0:def 2
.= (<*u*> ^ g1) . i by A4, A6, A28, A30, A33, A44, FINSEQ_1:23 ;
(<*u*> ^ g1) . (i + 1) = g1 . ((i + 1) - 1) by A43, A45, A46, FINSEQ_1:23
.= h . (x . (((len X) -' i) + 1)) by A25, A32, A37, A39, A50, FINSEQ_1:def 7 ;
hence ( Xi = X | (((len X) -' i) + 1) & h = (<*u*> ^ g1) . i & (<*u*> ^ g1) . (i + 1) = h . (x . (((len X) -' i) + 1)) ) by A37, A39, A40, A41, A51, FINSEQ_1:82; :: thesis:

end;

suppose i < 2 ; :: thesis:

then i < 1 + 1 ;
then A53: i <= 1 by NAT_1:13;
then A54: i = 1 by A30, XXREAL_0:1;
A55: len <*u*> = 1 by FINSEQ_1:40;
A56: i + 1 <= (len g1) + 1 by A4, A6, A28, A30, NAT_1:13;
A57: (<*u*> ^ g1) . (i + 1) = g1 . ((i + 1) - 1) by A54, A55, A56, FINSEQ_1:23
.= uxn1 by A30, A53, XXREAL_0:1, A28 ;
A58: (len X) -' i = (len X) - i by A30, XREAL_1:48, XREAL_0:def 2;
take X ; :: thesis:
take u ; :: thesis:
thus X = X | (((len X) -' i) + 1) by A54, A58, FINSEQ_1:58; :: thesis:
thus u = (<*u*> ^ g1) . i by A29, A30, A53, XXREAL_0:1; :: thesis:
thus (<*u*> ^ g1) . (i + 1) = u . (x . (((len X) -' i) + 1)) by A4, A54, A57, A58; :: thesis:

end;

consider K1 being RealNormSpace-Sequence, h1 being Point of (NestingLB (K1,Y)) such that
A59: ( K1 = <*(K . 1)*> & h1 = g1 . (len K) & (I0 . uxn1) . pk = h1 . (pk . 1) ) by A28;
A60: 1 in Seg n by A16;
then A61: <*(X . 1)*> = <*(K . 1)*> by FUNCT_1:49;
A62: 1 + (len <*u*>) <= (len K) + (len <*u*>) by A6, A16, XREAL_1:7;
A63: len <*u*> = 1 by FINSEQ_1:40;
A64: (<*u*> ^ g1) . (len X) = (<*u*> ^ g1) . ((len K) + 1) by A4, FINSEQ_3:53
.= g1 . (((len K) + 1) - 1) by A28, A62, A63, FINSEQ_1:23
.= g1 . (len K) ;
1 in dom pk by A27, A60, FINSEQ_1:def 3;
then A65: pk . 1 = x . 1 by A25, FINSEQ_1:def 7;
A66: I . u = I2 . (I1 . u) by A20, FUNCT_2:15;
reconsider v = I1 . u as Point of (R_NormSpace_of_BoundedLinearOperators ((X . n1),(R_NormSpace_of_BoundedMultilinearOperators (K,Y)))) by A20, FUNCT_2:5;
reconsider sn11 = xn1 as Point of (X . n1) ;
(I . u) . x = (I2 . v) . (pk ^ <*xn1*>) by A25, A26, A27, A66, FINSEQ_1:42
.= (v . sn11) . pk by A23
.= ((I0 * u1) . xn1) . pk by A20, A22
.= (I0 . uxn1) . pk by FUNCT_2:15 ;
hence ex X1 being RealNormSpace-Sequence ex h being Point of (NestingLB (X1,Y)) st
( X1 = <*(X . 1)*> & h = (<*u*> ^ g1) . (len X) & (I . u) . x = h . (x . 1) ) by A59, A61, A64, A65; :: thesis:

end;

A68: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
let X be RealNormSpace-Sequence; :: thesis:
consider I being Lipschitzian LinearOperator of (NestingLB (X,Y)),(R_NormSpace_of_BoundedMultilinearOperators (X,Y)) such that
A69: ( I is one-to-one & I is onto & I is isometric & ( for u being Point of (NestingLB (X,Y))
for x being Point of (product X) ex g being FinSequence st
( len g = len X & g . 1 = u & ( for i being Element of NAT st 1 <= i & i < len X holds
ex Xi being RealNormSpace-Sequence ex h being Point of (NestingLB (Xi,Y)) st
( Xi = X | (((len X) -' i) + 1) & h = g . i & g . (i + 1) = h . (x . (((len X) -' i) + 1)) ) ) & ex X1 being RealNormSpace-Sequence ex h being Point of (NestingLB (X1,Y)) st
( X1 = <*(X . 1)*> & h = g . (len X) & (I . u) . x = h . (x . 1) ) ) ) ) by A68, FINSEQ_1:20;
for u being Element of (NestingLB (X,Y)) holds ||.(I . u).|| = ||.u.|| by A69, NDIFF_7:7;
hence ex I being Lipschitzian LinearOperator of (NestingLB (X,Y)),(R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st
( I is one-to-one & I is onto & I is isometric & ( for u being Element of (NestingLB (X,Y)) holds ||.(I . u).|| = ||.u.|| ) & ( for u being Point of (NestingLB (X,Y))
for x being Point of (product X) ex g being FinSequence st
( len g = len X & g . 1 = u & ( for i being Element of NAT st 1 <= i & i < len X holds
ex Xi being RealNormSpace-Sequence ex h being Point of (NestingLB (Xi,Y)) st
( Xi = X | (((len X) -' i) + 1) & h = g . i & g . (i + 1) = h . (x . (((len X) -' i) + 1)) ) ) & ex X1 being RealNormSpace-Sequence ex h being Point of (NestingLB (X1,Y)) st
( X1 = <*(X . 1)*> & h = g . (len X) & (I . u) . x = h . (x . 1) ) ) ) ) by A69; :: thesis: