let I1, I2 be Lipschitzian LinearOperator of (NestingLB (X,Y)),(R_NormSpace_of_BoundedMultilinearOperators (X,Y)); :: thesis: ( I1 is one-to-one & I1 is onto & I1 is isometric & ( for u being Element of (NestingLB (X,Y)) holds ||.(I1 . 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) & (I1 . u) . x = h . (x . 1) ) ) ) & I2 is one-to-one & I2 is onto & I2 is isometric & ( for u being Element of (NestingLB (X,Y)) holds ||.(I2 . 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) & (I2 . u) . x = h . (x . 1) ) ) ) implies I1 = I2 )
assume A1: ( I1 is one-to-one & I1 is onto & I1 is isometric & ( for u being Element of (NestingLB (X,Y)) holds ||.(I1 . 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) & (I1 . u) . x = h . (x . 1) ) ) ) ) ; :: thesis: ( not I2 is one-to-one or not I2 is onto or not I2 is isometric or ex u being Element of (NestingLB (X,Y)) st not ||.(I2 . u).|| = ||.u.|| or ex u being Point of (NestingLB (X,Y)) ex x being Point of (product X) st
for g being FinSequence holds
( not len g = len X or not g . 1 = u or ex i being Element of NAT st
( 1 <= i & i < len X & ( for Xi being RealNormSpace-Sequence
for h being Point of (NestingLB (Xi,Y)) holds
( not Xi = X | (((len X) -' i) + 1) or not h = g . i or not g . (i + 1) = h . (x . (((len X) -' i) + 1)) ) ) ) or for X1 being RealNormSpace-Sequence
for h being Point of (NestingLB (X1,Y)) holds
( not X1 = <*(X . 1)*> or not h = g . (len X) or not (I2 . u) . x = h . (x . 1) ) ) or I1 = I2 )
assume A2: ( I2 is one-to-one & I2 is onto & I2 is isometric & ( for u being Element of (NestingLB (X,Y)) holds ||.(I2 . 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) & (I2 . u) . x = h . (x . 1) ) ) ) ) ; :: thesis: I1 = I2
for u being Point of (NestingLB (X,Y)) holds I1 . u = I2 . u

proof

let u be Point of (NestingLB (X,Y)); :: thesis: I1 . u = I2 . u
reconsider I1u = I1 . u, I2u = I2 . u as Multilinear Function of (product X),Y by LOPBAN10:def 11;

now :: thesis: for x being Point of (product X) holds I1u . x = I2u . x

let x be Point of (product X); :: thesis: I1u . x = I2u . x
consider g1 being FinSequence such that
A3: ( len g1 = len X & g1 . 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 = g1 . i & g1 . (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 = g1 . (len X) & (I1 . u) . x = h . (x . 1) ) ) by A1;
consider g2 being FinSequence such that
A4: ( len g2 = len X & g2 . 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 = g2 . i & g2 . (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 = g2 . (len X) & (I2 . u) . x = h . (x . 1) ) ) by A2;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len g1 implies g1 . $1 = g2 . $1 );
A5: S₁[ 0 ] ;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
assume A8: ( 1 <= k + 1 & k + 1 <= len g1 ) ; :: thesis: g1 . (k + 1) = g2 . (k + 1)

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: g1 . (k + 1) = g2 . (k + 1)

hence g1 . (k + 1) = g2 . (k + 1) by A3, A4; :: thesis: verum

end;

suppose A11: k <> 0 ; :: thesis: g1 . (k + 1) = g2 . (k + 1)

A12: k + 0 < k + 1 by XREAL_1:8;
then A13: k < len g1 by A8, XXREAL_0:2;
A15: k is Element of NAT by ORDINAL1:def 12;
k < len X by A3, A8, A12, XXREAL_0:2;
then A17: ex Xi being RealNormSpace-Sequence ex h being Point of (NestingLB (Xi,Y)) st
( Xi = X | (((len X) -' k) + 1) & h = g1 . k & g1 . (k + 1) = h . (x . (((len X) -' k) + 1)) ) by A3, A11, A15, NAT_1:14;
ex Xi being RealNormSpace-Sequence ex h being Point of (NestingLB (Xi,Y)) st
( Xi = X | (((len X) -' k) + 1) & h = g2 . k & g2 . (k + 1) = h . (x . (((len X) -' k) + 1)) ) by A3, A4, A11, A13, A15, NAT_1:14;
hence g1 . (k + 1) = g2 . (k + 1) by A7, A8, A11, A12, A17, NAT_1:14, XXREAL_0:2; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
hence I1u . x = I2u . x by A3, A4, FINSEQ_1:14; :: thesis: verum

end;

hence I1 . u = I2 . u by FUNCT_2:63; :: thesis: verum

end;

hence I1 = I2 ; :: thesis: verum