consider n being Element of NAT such that
A2: for m being Element of NAT
for x being Point of F1() st n <= m & x = F2() . m holds
P1[x] by A1;
( n in succ n & dom (F3() ") = NAT ) by FUNCT_2:def 1, ORDINAL1:6;
then (F3() ") . n in (F3() ") .: (succ n) by FUNCT_1:def 6;
then reconsider X = (F3() ") .: (succ n) as non empty finite Subset of NAT ;
reconsider mX = (max X) + 1 as Element of NAT ;
take mX ; :: thesis: for m being Element of NAT st mX <= m holds
P1[(F2() * F3()) . m]
let m be Element of NAT ; :: thesis: ( mX <= m implies P1[(F2() * F3()) . m] )
m in NAT ;
then A3: m in dom F3() by FUNCT_2:52;
assume A4: mX <= m ; :: thesis: P1[(F2() * F3()) . m]
n <= F3() . m
proof
assume F3() . m < n ; :: thesis: contradiction
then F3() . m in { p1 where p1 is Nat : p1 < n } ;
then F3() . m in n by AXIOMS:4;
then F3() . m in succ n by ORDINAL1:8;
then m in F3() " (succ n) by A3, FUNCT_1:def 7;
then m in (F3() ") .: (succ n) by FUNCT_1:85;
then m <= max X by XXREAL_2:def 8;
hence contradiction by A4, NAT_1:13; :: thesis: verum
end;
then A5: P1[F2() . (F3() . m)] by A2;
m in NAT ;
then m in dom F3() by FUNCT_2:def 1;
hence P1[(F2() * F3()) . m] by A5, FUNCT_1:13; :: thesis: verum