consider f being Function such that
A1: ( dom f = NAT & NestingLB (X,Y) = f . (len X) & f . 0 = Y & ( for j being Nat st j < len X holds
ex V being RealNormSpace ex k being Element of dom X st
( V = f . j & j + 1 = k & f . (j + 1) = R_NormSpace_of_BoundedLinearOperators ((X . k),V) ) ) ) by Def3;
for g being object st g in the carrier of (NestingLB (X,Y)) holds
g is Function

proof

let g be object ; :: thesis: ( g in the carrier of (NestingLB (X,Y)) implies g is Function )
assume A2: g in the carrier of (NestingLB (X,Y)) ; :: thesis: g is Function
1 <= len X by FINSEQ_1:20;
then (len X) - 1 in NAT by INT_1:3, XREAL_1:48;
then reconsider n = (len X) - 1 as Nat ;
(len X) - 1 < (len X) - 0 by XREAL_1:15;
then consider V being RealNormSpace, k being Element of dom X such that
A3: ( V = f . n & n + 1 = k & f . (n + 1) = R_NormSpace_of_BoundedLinearOperators ((X . k),V) ) by A1;
thus g is Function by A1, A2, A3; :: thesis: verum

end;

hence NestingLB (X,Y) is constituted-Functions by FUNCT_1:def 13, MONOID_0:80; :: thesis: verum