assume A4: F₃() <> F₄() ; :: thesis: contradiction
A5: dom F₃() = NAT by FUNCT_2:def 1;
dom F₄() = NAT by FUNCT_2:def 1;
then consider x being set such that
A6: ( x in NAT & F₃() . x <> F₄() . x ) by A4, A5, FUNCT_1:9;
defpred S₁[ Nat] means F₃() . $1 <> F₄() . $1;
A7: ex k being Nat st S₁[k] by A6;
consider m being Nat such that
A8: ( S₁[m] & ( for n being Nat st S₁[n] holds
m <= n ) ) from NAT_1:sch 5(A7);

now

assume m <> 0 ; :: thesis: contradiction
then consider k being Nat such that
A9: m = k + 1 by Th6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
k < m by A9, Th13;
then A10: F₃() . k = F₄() . k by A8;
( P₁[k,F₃() . k,F₃() . (k + 1)] & P₁[k,F₄() . k,F₄() . (k + 1)] ) by B2, B3;
hence contradiction by A3, A8, A9, A10; :: thesis: verum

end;

hence contradiction by A1, A2, A8; :: thesis: verum