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