defpred S₁[ Nat] means F₃() . $1 <> F₄() . $1;
A6: ( dom F₃() = NAT & dom F₄() = NAT ) by FUNCT_2:def 1;
assume F₃() <> F₄() ; :: thesis: contradiction
then ex x being object st
( x in NAT & F₃() . x <> F₄() . x ) by A6, FUNCT_1:2;
then A7: ex k being Nat st S₁[k] ;
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 :: thesis: not m <> 0

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 12;
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 A2, A4;
hence contradiction by A5, A8, A9, A10; :: thesis: verum

end;

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