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