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

let n be Element of NAT ; :: thesis:
assume A1: for x, y being Element of X
for k being Element of NAT st k = n holds
ex u being Element of X ex f being Function of NAT, the carrier of X st
( u = f . k & f . 0 = x & ( for j being Element of NAT st j < k holds
f . (j + 1) = (f . j) \ y ) ) ; :: thesis:
let x, y be Element of X; :: thesis:
let k be Element of NAT ; :: thesis:
consider u being Element of X, f being Function of NAT, the carrier of X such that
u = f . n and
A2: f . 0 = x and
A3: for j being Element of NAT st j < n holds
f . (j + 1) = (f . j) \ y by A1;
defpred S₂[ set , set ] means for j being Element of 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 Element of NAT ;

A5: now

assume A6: n + 1 <= i ; :: thesis:
take v = (f . n) \ y; :: thesis:
let j be Element of 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

assume A7: i < n + 1 ; :: thesis:
take v = f . k; :: thesis:
let j be Element of 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 Function of NAT, the carrier of X such that
A9: for k being Element of NAT holds S₂[k,f9 . k] from FUNCT_2:sch 3(A4);
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, A9; :: thesis:
let j be Element of NAT ; :: thesis:

A10: now

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

end;

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

A14: now

assume A15: j = n ; :: thesis:
then f99 . (j + 1) = (f . j) \ y by A9;
hence f99 . (j + 1) = (f99 . j) \ y by A13, A9, A15; :: thesis:

end;

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

end;

then A16: for n being Element of NAT st S₁[n] holds
S₁[n + 1] ;

now

let x, y be Element of X; :: thesis:
let n be Element of NAT ; :: thesis:
assume A17: n = 0 ; :: thesis:
reconsider f = NAT --> x as Function of NAT, 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 Element of NAT st j < n holds
f9 . (j + 1) = (f9 . j) \ y by A17, NAT_1:3; :: thesis:

end;

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