:: Isomorphism between Spaces of Multilinear Maps and Nested Compositions over Real Normed Vector Spaces
:: by Kazuhisa Nakasho and Yuichi Futa
::
:: Received April 30, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users

Th1: for X being RealLinearSpace-Sequence
for i being Element of dom X
for x being Element of (product X)
for r being Element of (X . i) holds (reproj (i,x)) . r = x +* (i,r)
by LOPBAN12:2;

definition

let X be RealLinearSpace;

func IsoCPRLSP X -> LinearOperator of X,(product <*X*>) means :Def1: :: LOPBAN14:def 1
for x being Point of X holds it . x = <*x*>;

existence
ex b₁ being LinearOperator of X,(product <*X*>) st
for x being Point of X holds b₁ . x = <*x*>

proof end;

uniqueness
for b₁, b₂ being LinearOperator of X,(product <*X*>) st ( for x being Point of X holds b₁ . x = <*x*> ) & ( for x being Point of X holds b₂ . x = <*x*> ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines IsoCPRLSP LOPBAN14:def 1 :
for X being RealLinearSpace
for b₂ being LinearOperator of X,(product <*X*>) holds
( b₂ = IsoCPRLSP X iff for x being Point of X holds b₂ . x = <*x*> );

theorem Th2: :: LOPBAN14:1

for X being RealLinearSpace holds 0. (product <*X*>) = (IsoCPRLSP X) . (0. X)

proof end;

registration

let X be RealLinearSpace;

cluster IsoCPRLSP X -> one-to-one onto ;

correctness
coherence
( IsoCPRLSP X is one-to-one & IsoCPRLSP X is onto );

proof end;

end;

registration

let X be RealLinearSpace;

cluster Relation-like the carrier of X -defined the carrier of (product <*X*>) -valued Function-like one-to-one empty total quasi_total onto additive homogeneous for Element of K19(K20( the carrier of X, the carrier of (product <*X*>)));

correctness
existence
ex b₁ being LinearOperator of X,(product <*X*>) st
( b₁ is one-to-one & b₁ is onto );

proof end;

end;

definition

let X be RealLinearSpace;
let f be bijective LinearOperator of X,(product <*X*>);
:: original: "
redefine func f " -> LinearOperator of (product <*X*>),X;
correctness
coherence
f " is LinearOperator of (product <*X*>),X;

proof end;

end;

registration

let X be RealLinearSpace;
let f be one-to-one onto LinearOperator of X,(product <*X*>);

cluster f " -> bijective for LinearOperator of (product <*X*>),X;

correctness
coherence
for b₁ being LinearOperator of (product <*X*>),X st b₁ = f " holds
b₁ is bijective ;

proof end;

end;

registration

let X be RealLinearSpace;

cluster Relation-like the carrier of (product <*X*>) -defined the carrier of X -valued Function-like one-to-one empty total) quasi_total onto additive homogeneous for Element of K19(K20( the carrier of (product <*X*>), the carrier of X));

correctness
existence
ex b₁ being LinearOperator of (product <*X*>),X st
( b₁ is one-to-one & b₁ is onto );

proof end;

end;

theorem :: LOPBAN14:2

for X being RealLinearSpace
for x being Point of X holds ((IsoCPRLSP X) ") . <*x*> = x

proof end;

theorem :: LOPBAN14:3

for X being RealLinearSpace holds ((IsoCPRLSP X) ") . (0. (product <*X*>)) = 0. X

proof end;

theorem :: LOPBAN14:4

for G being RealLinearSpace holds
( ( for x being set holds
( x is Point of (product <*G*>) iff ex x1 being Point of G st x = <*x1*> ) ) & ( for x, y being Point of (product <*G*>)
for x1, y1 being Point of G st x = <*x1*> & y = <*y1*> holds
x + y = <*(x1 + y1)*> ) & 0. (product <*G*>) = <*(0. G)*> & ( for x being Point of (product <*G*>)
for x1 being Point of G st x = <*x1*> holds
- x = <*(- x1)*> ) & ( for x being Point of (product <*G*>)
for x1 being Point of G
for a being Real st x = <*x1*> holds
a * x = <*(a * x1)*> ) )

proof end;

theorem Th6: :: LOPBAN14:5

for X, Y being RealLinearSpace
for f being Function of X,Y holds
( f is LinearOperator of X,Y iff f * ((IsoCPRLSP X) ") is LinearOperator of (product <*X*>),Y )

proof end;

theorem Th7: :: LOPBAN14:6

for X, Y being RealLinearSpace
for f being Function of (product <*X*>),Y holds
( f is LinearOperator of (product <*X*>),Y iff f * (IsoCPRLSP X) is LinearOperator of X,Y )

proof end;

theorem Th8: :: LOPBAN14:7

for X being RealLinearSpace
for s being Point of (product <*X*>)
for i being Element of dom <*X*> holds reproj (i,s) = IsoCPRLSP X

proof end;

theorem Th9: :: LOPBAN14:8

for X, Y being RealLinearSpace
for f being object holds
( f is LinearOperator of (product <*X*>),Y iff f is MultilinearOperator of <*X*>,Y )

proof end;

theorem Th10: :: LOPBAN14:9

for X, Y being RealLinearSpace holds MultilinearOperators (<*X*>,Y) = LinearOperators ((product <*X*>),Y)

proof end;

theorem :: LOPBAN14:10

for X, Y being RealLinearSpace holds R_VectorSpace_of_MultilinearOperators (<*X*>,Y) = R_VectorSpace_of_LinearOperators ((product <*X*>),Y)

proof end;

theorem Th12: :: LOPBAN14:11

for G being RealNormSpace holds
( ( for x being set holds
( x is Point of (product <*G*>) iff ex x1 being Point of G st x = <*x1*> ) ) & ( for x, y being Point of (product <*G*>)
for x1, y1 being Point of G st x = <*x1*> & y = <*y1*> holds
x + y = <*(x1 + y1)*> ) & 0. (product <*G*>) = <*(0. G)*> & ( for x being Point of (product <*G*>)
for x1 being Point of G st x = <*x1*> holds
- x = <*(- x1)*> ) & ( for x being Point of (product <*G*>)
for x1 being Point of G
for a being Real st x = <*x1*> holds
a * x = <*(a * x1)*> ) & ( for x being Point of (product <*G*>)
for x1 being Point of G st x = <*x1*> holds
||.x.|| = ||.x1.|| ) )

proof end;

definition

let X be RealNormSpace;

func IsoCPNrSP X -> LinearOperator of X,(product <*X*>) means :Def2: :: LOPBAN14:def 2
for x being Point of X holds it . x = <*x*>;

existence
ex b₁ being LinearOperator of X,(product <*X*>) st
for x being Point of X holds b₁ . x = <*x*>

proof end;

uniqueness
for b₁, b₂ being LinearOperator of X,(product <*X*>) st ( for x being Point of X holds b₁ . x = <*x*> ) & ( for x being Point of X holds b₂ . x = <*x*> ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines IsoCPNrSP LOPBAN14:def 2 :
for X being RealNormSpace
for b₂ being LinearOperator of X,(product <*X*>) holds
( b₂ = IsoCPNrSP X iff for x being Point of X holds b₂ . x = <*x*> );

theorem :: LOPBAN14:12

for X being RealNormSpace holds 0. (product <*X*>) = (IsoCPNrSP X) . (0. X)

proof end;

registration

let X be RealNormSpace;

cluster IsoCPNrSP X -> one-to-one onto isometric ;

correctness
coherence
( IsoCPNrSP X is one-to-one & IsoCPNrSP X is onto & IsoCPNrSP X is isometric );

proof end;

end;

registration

let X be RealNormSpace;

cluster Relation-like the carrier of X -defined the carrier of (product <*X*>) -valued Function-like one-to-one empty total quasi_total onto additive homogeneous isometric for Element of K19(K20( the carrier of X, the carrier of (product <*X*>)));

correctness
existence
ex b₁ being LinearOperator of X,(product <*X*>) st
( b₁ is one-to-one & b₁ is onto & b₁ is isometric );

proof end;

end;

definition

let X be RealNormSpace;
let I be one-to-one onto isometric LinearOperator of X,(product <*X*>);
:: original: "
redefine func I " -> LinearOperator of (product <*X*>),X;
correctness
coherence
I " is LinearOperator of (product <*X*>),X;

proof end;

end;

registration

let X be RealNormSpace;
let I be one-to-one onto isometric LinearOperator of X,(product <*X*>);

cluster I " -> one-to-one onto isometric for LinearOperator of (product <*X*>),X;

correctness
coherence
for b₁ being LinearOperator of (product <*X*>),X st b₁ = I " holds
( b₁ is one-to-one & b₁ is onto & b₁ is isometric );

proof end;

end;

registration

let X be RealNormSpace;

cluster Relation-like the carrier of (product <*X*>) -defined the carrier of X -valued Function-like one-to-one empty total) quasi_total onto additive homogeneous isometric for Element of K19(K20( the carrier of (product <*X*>), the carrier of X));

correctness
existence
ex b₁ being LinearOperator of (product <*X*>),X st
( b₁ is one-to-one & b₁ is onto & b₁ is isometric );

proof end;

end;

theorem Th14: :: LOPBAN14:13

for X, Y being RealNormSpace
for f being Function of X,Y holds
( f is LinearOperator of X,Y iff f * ((IsoCPNrSP X) ") is LinearOperator of (product <*X*>),Y )

proof end;

theorem Th15: :: LOPBAN14:14

for X, Y being RealNormSpace
for f being Function of X,Y holds
( f is Lipschitzian LinearOperator of X,Y iff f * ((IsoCPNrSP X) ") is Lipschitzian LinearOperator of (product <*X*>),Y )

proof end;

theorem Th16: :: LOPBAN14:15

for X, Y being RealNormSpace
for f being Function of (product <*X*>),Y holds
( f is LinearOperator of (product <*X*>),Y iff f * (IsoCPNrSP X) is LinearOperator of X,Y )

proof end;

theorem Th17: :: LOPBAN14:16

for X, Y being RealNormSpace
for f being Function of (product <*X*>),Y holds
( f is Lipschitzian LinearOperator of (product <*X*>),Y iff f * (IsoCPNrSP X) is Lipschitzian LinearOperator of X,Y )

proof end;

theorem Th18: :: LOPBAN14:17

for X being RealNormSpace
for s being Point of (product <*X*>)
for i being Element of dom <*X*> holds reproj (i,s) = IsoCPNrSP X

proof end;

theorem Th19: :: LOPBAN14:18

for X being RealNormSpace
for x being Point of (product <*X*>) holds NrProduct x = ||.x.||

proof end;

theorem Th20: :: LOPBAN14:19

for X, Y being RealNormSpace
for f being object holds
( f is LinearOperator of (product <*X*>),Y iff f is MultilinearOperator of <*X*>,Y )

proof end;

theorem Th21: :: LOPBAN14:20

for X, Y being RealNormSpace
for f being object holds
( f is Lipschitzian LinearOperator of (product <*X*>),Y iff f is Lipschitzian MultilinearOperator of <*X*>,Y )

proof end;

theorem Th22: :: LOPBAN14:21

for X, Y being RealNormSpace holds MultilinearOperators (<*X*>,Y) = LinearOperators ((product <*X*>),Y)

proof end;

theorem Th23: :: LOPBAN14:22

for X, Y being RealNormSpace holds BoundedMultilinearOperators (<*X*>,Y) = BoundedLinearOperators ((product <*X*>),Y)

proof end;

theorem Th24: :: LOPBAN14:23

for X, Y being RealNormSpace holds BoundedMultilinearOperatorsNorm (<*X*>,Y) = BoundedLinearOperatorsNorm ((product <*X*>),Y)

proof end;

theorem Th25: :: LOPBAN14:24

for X, Y being RealNormSpace holds R_VectorSpace_of_MultilinearOperators (<*X*>,Y) = R_VectorSpace_of_LinearOperators ((product <*X*>),Y)

proof end;

theorem Th26: :: LOPBAN14:25

for X, Y being RealNormSpace holds R_NormSpace_of_BoundedMultilinearOperators (<*X*>,Y) = R_NormSpace_of_BoundedLinearOperators ((product <*X*>),Y)

proof end;

theorem :: LOPBAN14:26

for X being RealNormSpace st X is complete holds
product <*X*> is complete

proof end;

theorem :: LOPBAN14:27

for X, Y being RealNormSpace-Sequence
for Z being RealNormSpace
for f being Lipschitzian BilinearOperator of (product X),(product Y),Z holds f * ((IsoCPNrSP ((product X),(product Y))) ") is Lipschitzian MultilinearOperator of <*(product X),(product Y)*>,Z by LOPBAN12:13;

theorem :: LOPBAN14:28

for X, Y being RealNormSpace-Sequence
for Z being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedBilinearOperators ((product X),(product Y),Z)) holds f * ((IsoCPNrSP ((product X),(product Y))) ") is Point of (R_NormSpace_of_BoundedMultilinearOperators (<*(product X),(product Y)*>,Z))

proof end;

theorem Th30: :: LOPBAN14:29

for X, Y being RealLinearSpace-Sequence holds carr (X ^ Y) = (carr X) ^ (carr Y)

proof end;

theorem Th31: :: LOPBAN14:30

for X being RealLinearSpace holds
( len (carr <*X*>) = len <*X*> & len (carr <*X*>) = 1 & carr <*X*> = <* the carrier of X*> )

proof end;

theorem Th32: :: LOPBAN14:31

for X being RealNormSpace-Sequence
for x being Element of (product X)
for Y being RealNormSpace
for z being Element of (product (X ^ <*Y*>))
for i being Element of dom X
for j being Element of dom (X ^ <*Y*>)
for xi being Element of (X . i)
for y being Point of Y st i = j & z = x ^ <*y*> holds
(reproj (j,z)) . xi = ((reproj (i,x)) . xi) ^ <*y*>

proof end;

theorem Th33: :: LOPBAN14:32

for X being RealNormSpace-Sequence
for x being Element of (product X)
for Y being RealNormSpace
for z being Element of (product (X ^ <*Y*>))
for j being Element of dom (X ^ <*Y*>)
for y being Element of Y
for y0 being Point of Y st z = x ^ <*y0*> & j = (len x) + 1 holds
(reproj (j,z)) . y = x ^ <*y*>

proof end;

theorem Th34: :: LOPBAN14:33

for X being RealNormSpace-Sequence
for x being Element of (product X)
for Y being RealNormSpace
for y being Point of Y holds x ^ <*y*> is Point of (product (X ^ <*Y*>))

proof end;

theorem Th35: :: LOPBAN14:34

for X being RealNormSpace-Sequence
for x being Element of (product X)
for Y being RealNormSpace
for z being Element of (product (X ^ <*Y*>))
for y being Point of Y st z = x ^ <*y*> holds
NrProduct z = ||.y.|| * (NrProduct x)

proof end;

theorem Th36: :: LOPBAN14:35

for X, Z being RealNormSpace
for Y being RealNormSpace-Sequence ex I being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,(R_NormSpace_of_BoundedMultilinearOperators (Y,Z)))),(R_NormSpace_of_BoundedMultilinearOperators ((Y ^ <*X*>),Z)) st
( I is one-to-one & I is onto & 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 ) ) ) )

proof end;

definition

let Y be RealNormSpace;
let X be RealNormSpace-Sequence;

func NestingLB (X,Y) -> RealNormSpace means :Def3: :: LOPBAN14:def 3
ex f being Function st
( dom f = NAT & it = f . (len X) & f . 0 = Y & ( for i being Nat st i < len X holds
ex fi being RealNormSpace ex j being Element of dom X st
( fi = f . i & i + 1 = j & f . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((X . j),fi) ) ) );

existence
ex b₁ being RealNormSpace ex f being Function st
( dom f = NAT & b₁ = f . (len X) & f . 0 = Y & ( for i being Nat st i < len X holds
ex fi being RealNormSpace ex j being Element of dom X st
( fi = f . i & i + 1 = j & f . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((X . j),fi) ) ) )

proof end;

uniqueness
for b₁, b₂ being RealNormSpace st ex f being Function st
( dom f = NAT & b₁ = f . (len X) & f . 0 = Y & ( for i being Nat st i < len X holds
ex fi being RealNormSpace ex j being Element of dom X st
( fi = f . i & i + 1 = j & f . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((X . j),fi) ) ) ) & ex f being Function st
( dom f = NAT & b₂ = f . (len X) & f . 0 = Y & ( for i being Nat st i < len X holds
ex fi being RealNormSpace ex j being Element of dom X st
( fi = f . i & i + 1 = j & f . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((X . j),fi) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines NestingLB LOPBAN14:def 3 :
for Y being RealNormSpace
for X being RealNormSpace-Sequence
for b₃ being RealNormSpace holds
( b₃ = NestingLB (X,Y) iff ex f being Function st
( dom f = NAT & b₃ = f . (len X) & f . 0 = Y & ( for i being Nat st i < len X holds
ex fi being RealNormSpace ex j being Element of dom X st
( fi = f . i & i + 1 = j & f . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((X . j),fi) ) ) ) );

theorem Th37: :: LOPBAN14:36

for X, Y, Z being RealNormSpace
for I being Lipschitzian LinearOperator of Y,Z st I is one-to-one & I is onto & I is isometric holds
ex L being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (X,Z)) st
( L is one-to-one & L is onto & L is isometric & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds L . f = I * f ) )

proof end;

theorem Th38: :: LOPBAN14:37

for X, Y, Z being RealNormSpace
for I being Lipschitzian LinearOperator of Y,Z st I is one-to-one & I is onto & I is isometric holds
ex L being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (Y,X)),(R_NormSpace_of_BoundedLinearOperators (Z,X)) st
( L is one-to-one & L is onto & L is isometric & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (Y,X)) holds L . f = f * (I ") ) )

proof end;

theorem Th39: :: LOPBAN14:38

for X, Y being RealNormSpace ex I being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators ((product <*X*>),Y)) st
( I is one-to-one & I is onto & I is isometric & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for x being Point of X holds (I . u) . <*x*> = u . x ) & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds ||.u.|| = ||.(I . u).|| ) )

proof end;

theorem :: LOPBAN14:39

for X, Y, Z, W being RealNormSpace
for I being Lipschitzian LinearOperator of X,Z
for J being Lipschitzian LinearOperator of Y,W st I is one-to-one & I is onto & I is isometric & J is one-to-one & J is onto & J is isometric holds
ex K being Lipschitzian LinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Z,W)) st
( K is one-to-one & K is onto & K is isometric & ( for x being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds K . x = J * (x * (I ")) ) )

proof end;

theorem Th41: :: LOPBAN14:40

for n being Nat
for A, B being RealNormSpace-Sequence
for X, Y being RealNormSpace st len A = n + 1 & A | n = B & X = A . (n + 1) holds
NestingLB (A,Y) = R_NormSpace_of_BoundedLinearOperators (X,(NestingLB (B,Y)))

proof end;

registration

let Y be RealNormSpace;
let X be RealNormSpace-Sequence;

cluster NestingLB (X,Y) -> constituted-Functions ;

coherence
NestingLB (X,Y) is constituted-Functions

proof end;

end;

Lm1: for Y being RealNormSpace
for X being RealNormSpace-Sequence 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) ) ) ) )

proof end;

definition

let Y be RealNormSpace;
let X be RealNormSpace-Sequence;

func NestMult (X,Y) -> Lipschitzian LinearOperator of (NestingLB (X,Y)),(R_NormSpace_of_BoundedMultilinearOperators (X,Y)) means :: LOPBAN14:def 4
( it is one-to-one & it is onto & it is isometric & ( for u being Element of (NestingLB (X,Y)) holds ||.(it . 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) & (it . u) . x = h . (x . 1) ) ) ) );

existence
ex b₁ being Lipschitzian LinearOperator of (NestingLB (X,Y)),(R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st
( b₁ is one-to-one & b₁ is onto & b₁ is isometric & ( for u being Element of (NestingLB (X,Y)) holds ||.(b₁ . 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) & (b₁ . u) . x = h . (x . 1) ) ) ) ) by Lm1;
uniqueness
for b₁, b₂ being Lipschitzian LinearOperator of (NestingLB (X,Y)),(R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st b₁ is one-to-one & b₁ is onto & b₁ is isometric & ( for u being Element of (NestingLB (X,Y)) holds ||.(b₁ . 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) & (b₁ . u) . x = h . (x . 1) ) ) ) & b₂ is one-to-one & b₂ is onto & b₂ is isometric & ( for u being Element of (NestingLB (X,Y)) holds ||.(b₂ . 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) & (b₂ . u) . x = h . (x . 1) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines NestMult LOPBAN14:def 4 :
for Y being RealNormSpace
for X being RealNormSpace-Sequence
for b₃ being Lipschitzian LinearOperator of (NestingLB (X,Y)),(R_NormSpace_of_BoundedMultilinearOperators (X,Y)) holds
( b₃ = NestMult (X,Y) iff ( b₃ is one-to-one & b₃ is onto & b₃ is isometric & ( for u being Element of (NestingLB (X,Y)) holds ||.(b₃ . 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) & (b₃ . u) . x = h . (x . 1) ) ) ) ) );