defpred S₁[ Nat] means P₁[F₁() * $1];
A4: S₁[ 0 ] by A1;

A5: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A6: S₁[i] ; :: thesis: S₁[i + 1]
F₁() * (i + 1) = (F₁() * i) + F₁() ;
hence S₁[i + 1] by A2, A3, A6; :: thesis: verum

end;

A7: for i being Nat holds S₁[i] from NAT_1:sch 2(A4, A5);

per cases ( F₂() mod F₁() = 0 or F₂() mod F₁() <> 0 ) ;

suppose F₂() mod F₁() = 0 ; :: thesis: P₁[F₂()]

then F₂() = (F₁() * (F₂() div F₁())) + 0 by A2, INT_1:59;
hence P₁[F₂()] by A7; :: thesis: verum

end;

suppose A8: F₂() mod F₁() <> 0 ; :: thesis: P₁[F₂()]

A9: F₂() = (F₁() * (F₂() div F₁())) + (F₂() mod F₁()) by A2, INT_1:59;
F₂() mod F₁() <= F₁() by A2, Th1;
hence P₁[F₂()] by A3, A7, A8, A9; :: thesis: verum

end;

end;