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 Nat
for x being set ex y being set st S1[n,x,y]
proof
let n be
Nat;
for x being set ex y being set st S1[n,x,y]let x be
set ;
ex y being set st S1[n,x,y]
end;
consider g being Function such that
A7:
dom g = NAT
and
A8:
g . 0 = n0
and
A9:
for n being Nat holds S1[n,g . n,g . (n + 1)]
from RECDEF_1:sch 1(A3);
rng g c= NAT
then reconsider g = g as sequence of NAT by A7, FUNCT_2:2;
g is V46()
by A9;
then reconsider g = g as V46() 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
; for n being Element of NAT holds P1[S1 . n]
thus
for n being Element of NAT holds P1[S1 . n]
verum