defpred S₁[ set ] means for x, y being Element of X
for n being Nat st n = $1 holds
ex u being Element of X ex f being sequence of the carrier of X st
( u = f . n & f . 0 = x & ( for j being Nat st j < n holds
f . (j + 1) = (f . j) \ y ) );

let n be Nat; :: thesis:
assume A1: for x, y being Element of X
for k being Nat st k = n holds
ex u being Element of X ex f being sequence of the carrier of X st
( u = f . k & f . 0 = x & ( for j being Nat st j < k holds
f . (j + 1) = (f . j) \ y ) ) ; :: thesis:
let x, y be Element of X; :: thesis:
let k be Nat; :: thesis:
consider u being Element of X, f being sequence of the carrier of X such that
u = f . n and
A2: f . 0 = x and
A3: for j being Nat st j < n holds
f . (j + 1) = (f . j) \ y by A1;
defpred S₂[ set , set ] means for j being Nat st $1 = j holds
( ( j < n + 1 implies $2 = f . $1 ) & ( n + 1 <= j implies $2 = (f . n) \ y ) );
assume k = n + 1 ; :: thesis:
A4: for k being Element of NAT ex v being Element of X st S₂[k,v]

let k be Element of NAT ; :: thesis:
reconsider i = k as Nat ;

A5: now :: thesis:

assume A6: n + 1 <= i ; :: thesis:
take v = (f . n) \ y; :: thesis:
let j be Nat; :: thesis:
assume k = j ; :: thesis:
hence ( j < n + 1 implies v = f . k ) by A6; :: thesis:
assume n + 1 <= j ; :: thesis:
thus v = (f . n) \ y ; :: thesis:

end;

now :: thesis:

assume A7: i < n + 1 ; :: thesis:
take v = f . k; :: thesis:
let j be Nat; :: thesis:
assume A8: k = j ; :: thesis:
thus ( j < n + 1 implies v = f . k ) ; :: thesis:
thus ( n + 1 <= j implies v = (f . n) \ y ) by A7, A8; :: thesis:

end;

hence ex v being Element of X st S₂[k,v] by A5; :: thesis:

end;

consider f9 being sequence of the carrier of X such that
A9: for k being Element of NAT holds S₂[k,f9 . k] from FUNCT_2:sch 3(A4);
A10: for k being Nat holds S₂[k,f9 . k]

proof

let k be Nat; :: thesis:
k in NAT by ORDINAL1:def 12;
hence S₂[k,f9 . k] by A9; :: thesis:

end;

take z = f9 . (n + 1); :: thesis:
take f99 = f9; :: thesis:
thus z = f99 . (n + 1) ; :: thesis:
0 < n + 1 by NAT_1:5;
hence f99 . 0 = x by A2, A10; :: thesis:
let j be Nat; :: thesis:

A11: now :: thesis:

assume A12: j < n ; :: thesis:
then ( f . (j + 1) = (f . j) \ y & j < n + 1 ) by A3, NAT_1:13;
then A13: f . (j + 1) = (f9 . j) \ y by A10;
j + 1 < n + 1 by A12, XREAL_1:6;
hence f99 . (j + 1) = (f99 . j) \ y by A10, A13; :: thesis:

end;

A14: n < n + 1 by NAT_1:13;

A15: now :: thesis:

assume A16: j = n ; :: thesis:
then f99 . (j + 1) = (f . j) \ y by A10;
hence f99 . (j + 1) = (f99 . j) \ y by A14, A10, A16; :: thesis:

end;

assume j < n + 1 ; :: thesis:
then j <= n by NAT_1:13;
hence f99 . (j + 1) = (f99 . j) \ y by A11, A15, XXREAL_0:1; :: thesis:

end;

then A17: for n being Nat st S₁[n] holds
S₁[n + 1] ;

now :: thesis:

let x, y be Element of X; :: thesis:
let n be Nat; :: thesis:
assume A18: n = 0 ; :: thesis:
reconsider f = NAT --> x as sequence of the carrier of X ;
take u = f . n; :: thesis:
take f9 = f; :: thesis:
thus ( u = f9 . n & f9 . 0 = x ) by FUNCOP_1:7; :: thesis:
thus for j being Nat st j < n holds
f9 . (j + 1) = (f9 . j) \ y by A18, NAT_1:3; :: thesis:

end;

then A19: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A19, A17);
hence ex b₁ being Element of X ex f being sequence of the carrier of X st
( b₁ = f . n & f . 0 = x & ( for j being Nat st j < n holds
f . (j + 1) = (f . j) \ y ) ) ; :: thesis: