consider n being Element of NAT such that
A2: for m being Element of NAT
for x being Point of F₁() st n <= m & x = F₂() . m holds
P₁[x] by A1;
( n in succ n & dom (F₃() ") = NAT ) by FUNCT_2:def 1, ORDINAL1:6;
then (F₃() ") . n in (F₃() ") .: (succ n) by FUNCT_1:def 6;
then reconsider X = (F₃() ") .: (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
P₁[(F₂() * F₃()) . m]
let m be Element of NAT ; :: thesis: ( mX <= m implies P₁[(F₂() * F₃()) . m] )
m in NAT ;
then A3: m in dom F₃() by FUNCT_2:52;
assume A4: mX <= m ; :: thesis: P₁[(F₂() * F₃()) . m]
n <= F₃() . m

proof

assume F₃() . m < n ; :: thesis: contradiction
then F₃() . m in { p1 where p1 is Nat : p1 < n } ;
then F₃() . m in n by AXIOMS:4;
then F₃() . m in succ n by ORDINAL1:8;
then m in F₃() " (succ n) by A3, FUNCT_1:def 7;
then m in (F₃() ") .: (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: P₁[F₂() . (F₃() . m)] by A2;
m in NAT ;
then m in dom F₃() by FUNCT_2:def 1;
hence P₁[(F₂() * F₃()) . m] by A5, FUNCT_1:13; :: thesis: verum