defpred S₁[ set ] means for X being RealNormSpace-Sequence st len X = $1 holds
ex fn being RealNormSpace ex f being Function st
( dom f = NAT & fn = 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) ) ) );
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A2: for X being RealNormSpace-Sequence st len X = n holds
ex fn being RealNormSpace ex f being Function st
( dom f = NAT & fn = 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) ) ) ) ; :: thesis:
let X be RealNormSpace-Sequence; :: thesis:
assume A3: len X = n + 1 ; :: thesis:
then A4: dom X = Seg (n + 1) by FINSEQ_1:def 3;
then A5: n + 1 in dom X by FINSEQ_1:4;
reconsider n1 = n + 1 as Element of dom X by A4, FINSEQ_1:4;

end;

set XN = X | n;
A13: n < n + 1 by NAT_1:13;
for x being set st x in rng (X | n) holds
x is RealNormSpace

end;

then reconsider XN = X | n as RealNormSpace-Sequence by A12, PRVECT_2:def 10;
consider fn being RealNormSpace, f being Function such that
A14: ( dom f = NAT & fn = f . (len XN) & f . 0 = Y ) and
A15: for i being Nat st i < len XN holds
ex fi being RealNormSpace ex j being Element of dom XN st
( fi = f . i & i + 1 = j & f . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((XN . j),fi) ) by A2, A3, A13, FINSEQ_1:59;
defpred S₂[ object , object ] means for i being Nat st $1 = i holds
( ( i < n + 1 implies $2 = f . $1 ) & ( n + 1 <= i implies ex xn1, fn being RealNormSpace st
( xn1 = X . (n + 1) & fn = f . (len XN) & $2 = R_NormSpace_of_BoundedLinearOperators (xn1,fn) ) ) );
A16: for x, y1, y2 being object st x in NAT & S₂[x,y1] & S₂[x,y2] holds
y1 = y2

let x, y1, y2 be object ; :: thesis:
assume A17: ( x in NAT & S₂[x,y1] & S₂[x,y2] ) ; :: thesis:
reconsider i = x as Nat by A17;

hence y1 = f . x by A17
.= y2 by A17, A18 ;
:: thesis:

end;

end;

A21: for x being object st x in NAT holds
ex y being object st S₂[x,y]

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider x0 = x as Nat ;

take y2 = f . x; :: thesis:
let i be Nat; :: thesis:
assume A23: x = i ; :: thesis:
thus ( i < n + 1 implies y2 = f . x ) ; :: thesis:
thus ( n + 1 <= i implies ex xn1, fn being RealNormSpace st
( xn1 = X . (n + 1) & fn = f . (len XN) & y2 = R_NormSpace_of_BoundedLinearOperators (xn1,fn) ) ) by A22, A23; :: thesis:

end;

X . (n + 1) in rng X by A5, FUNCT_1:def 3;
then reconsider xn1 = X . (n + 1) as RealNormSpace by PRVECT_2:def 10;
take y2 = R_NormSpace_of_BoundedLinearOperators (xn1,fn); :: thesis:
let i be Nat; :: thesis:
assume x = i ; :: thesis:
hence ( i < n + 1 implies y2 = f . x ) by A24; :: thesis:
thus ( n + 1 <= i implies ex xn1, fn being RealNormSpace st
( xn1 = X . (n + 1) & fn = f . (len XN) & y2 = R_NormSpace_of_BoundedLinearOperators (xn1,fn) ) ) by A14; :: thesis:

end;

consider f1 being Function such that
A26: dom f1 = NAT and
A27: for j being object st j in NAT holds
S₂[j,f1 . j] from FUNCT_1:sch 2(A16, A21);
A28: for j being Nat holds S₂[j,f1 . j]

end;

end;

assume A37: i < n ; :: thesis:
then A38: i + 1 < n + 1 by XREAL_1:6;
i < len XN by A3, A13, A37, FINSEQ_1:17;
then consider fi being RealNormSpace, j being Element of dom XN such that
A39: ( fi = f . i & i + 1 = j & f . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((XN . j),fi) ) by A15;
i < n + 1 by A37, NAT_1:13;
then A40: f2 . i = f . i by A28;
reconsider j0 = j as Element of dom X by RELAT_1:60, TARSKI:def 3;
A41: X . j0 = XN . j by FUNCT_1:47;
f2 . (i + 1) = f . (i + 1) by A28, A38;
hence ex fi being RealNormSpace ex j0 being Element of dom X st
( fi = f2 . i & i + 1 = j0 & f2 . (i + 1) = R_NormSpace_of_BoundedLinearOperators ((X . j0),fi) ) by A39, A40, A41; :: thesis:

end;

end;

reconsider f = NAT --> Y as Function ;
let X be RealNormSpace-Sequence; :: thesis:
assume A43: len X = 0 ; :: thesis:
reconsider fn = f . (len X) as RealNormSpace ;
take fn ; :: thesis:
take f ; :: thesis:
thus dom f = NAT ; :: thesis:
thus ( fn = f . (len X) & f . 0 = Y ) ; :: thesis:
let i be Nat; :: thesis:
assume i < len X ; :: thesis:
hence 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) ) by A43, NAT_1:2; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A42, A1);
hence ex fn being RealNormSpace ex f being Function st
( dom f = NAT & fn = 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) ) ) ) ; :: thesis: