let m, n be Element of NAT ; :: thesis: seq (m,n),n are_equipotent
defpred S1[ Nat] means seq (m,\$1),\$1 are_equipotent ;
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: seq (m,n),n are_equipotent ; :: thesis: S1[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 ;
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 ;
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 ;
hence S1[n + 1] by ; :: thesis: verum
end;
A11: S1[ 0 ] by Th2;
for n being Nat holds S1[n] from NAT_1:sch 2(A11, A1);
hence seq (m,n),n are_equipotent ; :: thesis: verum