let m, n be Element of NAT ; :: thesis: seq (m,n),n are_equipotent
defpred S₁[ Nat] means seq (m,$1),$1 are_equipotent ;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: seq (m,n),n are_equipotent ; :: thesis: S₁[n + 1]
reconsider i = m + n as Nat ;
A3: Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;

A4: now :: thesis: not seq (m,n) meets {(i + 1)}

assume seq (m,n) meets {(i + 1)} ; :: thesis: contradiction
then consider x being object such that
A5: x in seq (m,n) and
A6: x in {(i + 1)} by XBOOLE_0:3;
A7: not i + 1 <= i by NAT_1:13;
x = i + 1 by A6, TARSKI:def 1;
hence contradiction by A5, A7, Th1; :: thesis: verum

end;

A8: now :: thesis: not n meets {n}

assume n meets {n} ; :: thesis: contradiction
then consider x being object such that
A9: x in n and
A10: x in {n} by XBOOLE_0:3;
A: x = n by A10, TARSKI:def 1;
reconsider x = x as set by TARSKI:1;
not x in x ;
hence contradiction by A, A9; :: thesis: verum

end;

( seq (m,(n + 1)) = (seq (m,n)) \/ {(i + 1)} & {(i + 1)},{n} are_equipotent ) by Th5, CARD_1:28;
hence S₁[n + 1] by A2, A3, A8, A4, CARD_1:31; :: thesis: verum

end;

A11: S₁[ 0 ] by Th2;
for n being Nat holds S₁[n] from NAT_1:sch 2(A11, A1);
hence seq (m,n),n are_equipotent ; :: thesis: verum