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

proof

let n be Element of 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 Element of NAT ;
A3: n + 1 = succ n by NAT_1:38
.= n \/ {n} by ORDINAL1:def 1 ;

A4: now

assume seq (m,n) meets {(i + 1)} ; :: thesis: contradiction
then consider x being set 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

assume n meets {n} ; :: thesis: contradiction
then consider x being set such that
A9: x in n and
A10: x in {n} by XBOOLE_0:3;
x = n by A10, TARSKI:def 1;
hence contradiction by 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 Element of NAT holds S₁[n] from NAT_1:sch 1(A11, A1);
hence seq (m,n),n are_equipotent ; :: thesis: verum