defpred S1[ set , set , set ] means ( $3 in NAT & ( for m, k being Element of NAT st m = $2 & k = $3 holds
( m < k & P1[F2() . k] ) ) );
consider n0 being Element of NAT such that
0 <= n0 and
A2: P1[F2() . n0] by A1;
A3: for n being Element of NAT
for x being set ex y being set st S1[n,x,y]
proof
let n be Element of NAT ; :: thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; :: thesis: ex y being set st S1[n,x,y]
per cases ( x in NAT or not x in NAT ) ;
suppose x in NAT ; :: thesis: ex y being set st S1[n,x,y]
then reconsider mx = x as Element of NAT ;
consider my being Element of NAT such that
A4: ( mx + 1 <= my & P1[F2() . my] ) by A1;
take my ; :: thesis: S1[n,x,my]
thus my in NAT ; :: thesis: for m, k being Element of NAT st m = x & k = my holds
( m < k & P1[F2() . k] )
thus for m, k being Element of NAT st m = x & k = my holds
( m < k & P1[F2() . k] ) by A4, NAT_1:13; :: thesis: verum
end;
suppose A5: not x in NAT ; :: thesis: ex y being set st S1[n,x,y]
take 0 ; :: thesis: S1[n,x, 0 ]
set y = 0 ;
thus 0 in NAT ; :: thesis: for m, k being Element of NAT st m = x & k = 0 holds
( m < k & P1[F2() . k] )
let m, k be Element of NAT ; :: thesis: ( m = x & k = 0 implies ( m < k & P1[F2() . k] ) )
assume that
A6: m = x and
k = 0 ; :: thesis: ( m < k & P1[F2() . k] )
thus ( m < k & P1[F2() . k] ) by A5, A6; :: thesis: verum
end;
end;
end;
consider g being Function such that
A7: dom g = NAT and
A8: g . 0 = n0 and
A9: for n being Element of NAT holds S1[n,g . n,g . (n + 1)] from RECDEF_1:sch 1(A3);
 rng g c= NAT
proof
defpred S2[ Element of NAT ] means g . $1 in NAT ;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in NAT )
assume y in rng g ; :: thesis: y in NAT
then consider x being set such that
A10: x in dom g and
A11: g . x = y by FUNCT_1:def 5;
reconsider n = x as Element of NAT by A7, A10;
A12: for k being Element of NAT st S2[k] holds
S2[k + 1] by A9;
A13: S2[ 0 ] by A8;
for k being Element of NAT holds S2[k] from NAT_1:sch 1(A13, A12);
 then g . n in NAT ;
hence y in NAT by A11; :: thesis: verum
end;
then reconsider g = g as sequence of NAT by A7, FUNCT_2:4;
g is increasing
proof
let n be Nat; :: according to VALUED_1:def 13 :: thesis: g . n < g . (n + 1)
reconsider n = n as Element of NAT by ORDINAL1:def 13;
g . n < g . (n + 1) by A9;
hence g . n < g . (n + 1) ; :: thesis: verum
end;
then reconsider g = g as V34() sequence of NAT ;
reconsider S1 = F2() * g as sequence of F1() ;
A14: dom S1 = NAT by FUNCT_2:def 1;
reconsider S1 = S1 as subsequence of F2() ;
take S1 ; :: thesis: for n being Element of NAT holds P1[S1 . n]
thus for n being Element of NAT holds P1[S1 . n] :: thesis: verum
proof
let n be Element of NAT ; :: thesis: P1[S1 . n]
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: P1[S1 . n]
hence P1[S1 . n] by A2, A8, A14, FUNCT_1:22; :: thesis: verum
end;
suppose n <> 0 ; :: thesis: P1[S1 . n]
then n >= 0 + 1 by NAT_1:13;
then reconsider n' = n - 1 as Element of NAT by INT_1:18;
reconsider k = g . (n' + 1) as Element of NAT ;
for m, k being Element of NAT st m = g . n' & k = g . (n' + 1) holds
P1[F2() . k] by A9;
then P1[F2() . k] ;
hence P1[S1 . n] by A14, FUNCT_1:22; :: thesis: verum
end;
end;
end;