:: 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) ) ) ) ) );