let m, n be Element of NAT ; :: thesis: seq (m,n),n are_equipotent

defpred S_{1}[ Nat] means seq (m,$1),$1 are_equipotent ;

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
by Th2;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A11, A1);

hence seq (m,n),n are_equipotent ; :: thesis: verum

defpred S

A1: for n being Nat st S

S

proof

A11:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: seq (m,n),n are_equipotent ; :: thesis: S_{1}[n + 1]

reconsider i = m + n as Nat ;

A3: Segm (n + 1) = (Segm n) \/ {n} by AFINSQ_1:2;

hence S_{1}[n + 1]
by A2, A3, A8, A4, CARD_1:31; :: thesis: verum

end;assume A2: seq (m,n),n are_equipotent ; :: thesis: S

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;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

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

( seq (m,(n + 1)) = (seq (m,n)) \/ {(i + 1)} & {(i + 1)},{n} are_equipotent )
by Th5, CARD_1:28;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;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

hence S

for n being Nat holds S

hence seq (m,n),n are_equipotent ; :: thesis: verum