let m be Nat; :: thesis: for n being Nat

for F being finite set st F = { k where k is Nat : ( m <= k & k <= m + n ) } holds

card F = n + 1

defpred S_{1}[ Nat] means for F being finite set st F = { k where k is Nat : ( m <= k & k <= m + $1 ) } holds

card F = $1 + 1;

_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A16, A1);

hence for n being Nat

for F being finite set st F = { k where k is Nat : ( m <= k & k <= m + n ) } holds

card F = n + 1 ; :: thesis: verum

for F being finite set st F = { k where k is Nat : ( m <= k & k <= m + n ) } holds

card F = n + 1

defpred S

card F = $1 + 1;

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

S_{1}[n + 1]

A16:
SS

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

assume A2: S_{1}[n]
; :: thesis: S_{1}[n + 1]

thus S_{1}[n + 1]
:: thesis: verum

end;assume A2: S

thus S

proof

A3:
succ (Segm (m + n)) = { k where k is Nat : k <= m + n }
by NAT_1:54;

set F1 = { k where k is Nat : ( m <= k & k <= m + n ) } ;

{ k where k is Nat : ( m <= k & k <= m + n ) } c= succ (Segm (m + n))

let F be finite set ; :: thesis: ( F = { k where k is Nat : ( m <= k & k <= m + (n + 1) ) } implies card F = (n + 1) + 1 )

A4: not m + (n + 1) in { k where k is Nat : ( m <= k & k <= m + n ) }

card F1 = n + 1 by A2;

hence card F = (n + 1) + 1 by A15, A4, CARD_2:41; :: thesis: verum

end;set F1 = { k where k is Nat : ( m <= k & k <= m + n ) } ;

{ k where k is Nat : ( m <= k & k <= m + n ) } c= succ (Segm (m + n))

proof

then reconsider F1 = { k where k is Nat : ( m <= k & k <= m + n ) } as finite set ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : ( m <= k & k <= m + n ) } or x in succ (Segm (m + n)) )

assume x in { k where k is Nat : ( m <= k & k <= m + n ) } ; :: thesis: x in succ (Segm (m + n))

then ex k being Nat st

( x = k & m <= k & k <= m + n ) ;

hence x in succ (Segm (m + n)) by A3; :: thesis: verum

end;assume x in { k where k is Nat : ( m <= k & k <= m + n ) } ; :: thesis: x in succ (Segm (m + n))

then ex k being Nat st

( x = k & m <= k & k <= m + n ) ;

hence x in succ (Segm (m + n)) by A3; :: thesis: verum

let F be finite set ; :: thesis: ( F = { k where k is Nat : ( m <= k & k <= m + (n + 1) ) } implies card F = (n + 1) + 1 )

A4: not m + (n + 1) in { k where k is Nat : ( m <= k & k <= m + n ) }

proof

assume A5:
F = { k where k is Nat : ( m <= k & k <= m + (n + 1) ) }
; :: thesis: card F = (n + 1) + 1
assume
m + (n + 1) in { k where k is Nat : ( m <= k & k <= m + n ) }
; :: thesis: contradiction

then ex k being Nat st

( m + (n + 1) = k & m <= k & k <= m + n ) ;

then (m + n) + 1 <= (m + n) + 0 ;

hence contradiction by XREAL_1:6; :: thesis: verum

end;then ex k being Nat st

( m + (n + 1) = k & m <= k & k <= m + n ) ;

then (m + n) + 1 <= (m + n) + 0 ;

hence contradiction by XREAL_1:6; :: thesis: verum

now :: thesis: for x being object holds

( ( x in F implies x in F1 \/ {(m + (n + 1))} ) & ( x in F1 \/ {(m + (n + 1))} implies x in F ) )

then A15:
F = { k where k is Nat : ( m <= k & k <= m + n ) } \/ {(m + (n + 1))}
by TARSKI:2;( ( x in F implies x in F1 \/ {(m + (n + 1))} ) & ( x in F1 \/ {(m + (n + 1))} implies x in F ) )

let x be object ; :: thesis: ( ( x in F implies x in F1 \/ {(m + (n + 1))} ) & ( x in F1 \/ {(m + (n + 1))} implies b_{1} in F ) )

_{1} in F

end;hereby :: thesis: ( x in F1 \/ {(m + (n + 1))} implies b_{1} in F )

assume A9:
x in F1 \/ {(m + (n + 1))}
; :: thesis: bassume
x in F
; :: thesis: x in F1 \/ {(m + (n + 1))}

then consider k being Nat such that

A6: x = k and

A7: m <= k and

A8: k <= m + (n + 1) by A5;

k <= (m + n) + 1 by A8;

then ( k <= m + n or k = m + (n + 1) ) by NAT_1:8;

then ( k in F1 or k in {(m + (n + 1))} ) by A7, TARSKI:def 1;

hence x in F1 \/ {(m + (n + 1))} by A6, XBOOLE_0:def 3; :: thesis: verum

end;then consider k being Nat such that

A6: x = k and

A7: m <= k and

A8: k <= m + (n + 1) by A5;

k <= (m + n) + 1 by A8;

then ( k <= m + n or k = m + (n + 1) ) by NAT_1:8;

then ( k in F1 or k in {(m + (n + 1))} ) by A7, TARSKI:def 1;

hence x in F1 \/ {(m + (n + 1))} by A6, XBOOLE_0:def 3; :: thesis: verum

card F1 = n + 1 by A2;

hence card F = (n + 1) + 1 by A15, A4, CARD_2:41; :: thesis: verum

proof

for n being Nat holds S
let F be finite set ; :: thesis: ( F = { k where k is Nat : ( m <= k & k <= m + 0 ) } implies card F = 0 + 1 )

assume A17: F = { k where k is Nat : ( m <= k & k <= m + 0 ) } ; :: thesis: card F = 0 + 1

hence card F = 0 + 1 by CARD_1:30; :: thesis: verum

end;assume A17: F = { k where k is Nat : ( m <= k & k <= m + 0 ) } ; :: thesis: card F = 0 + 1

now :: thesis: for x being object holds

( ( x in F implies x = m ) & ( x = m implies x in F ) )

then
F = {m}
by TARSKI:def 1;( ( x in F implies x = m ) & ( x = m implies x in F ) )

let x be object ; :: thesis: ( ( x in F implies x = m ) & ( x = m implies x in F ) )

hence x in F by A17; :: thesis: verum

end;hereby :: thesis: ( x = m implies x in F )

assume
x = m
; :: thesis: x in Fassume
x in F
; :: thesis: x = m

then ex k being Nat st

( x = k & m <= k & k <= m + 0 ) by A17;

hence x = m by XXREAL_0:1; :: thesis: verum

end;then ex k being Nat st

( x = k & m <= k & k <= m + 0 ) by A17;

hence x = m by XXREAL_0:1; :: thesis: verum

hence x in F by A17; :: thesis: verum

hence card F = 0 + 1 by CARD_1:30; :: thesis: verum

hence for n being Nat

for F being finite set st F = { k where k is Nat : ( m <= k & k <= m + n ) } holds

card F = n + 1 ; :: thesis: verum