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₁[ Nat] means for F being finite set st F = { k where k is Nat : ( m <= k & k <= m + $1 ) } holds
card F = $1 + 1;

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

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

proof

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;

then reconsider F1 = { k where k is Nat : ( m <= k & k <= m + n ) } as finite set ;
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 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;

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

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

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

hereby :: thesis: ( x in F1 \/ {(m + (n + 1))} implies b₁ in F )

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

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

per cases ( x in F1 or x in {(m + (n + 1))} ) by A9, XBOOLE_0:def 3;

suppose x in F1 ; :: thesis: b₁ in F

then consider k being Nat such that
A10: x = k and
A11: m <= k and
A12: k <= m + n ;
k <= (m + n) + 1 by A12, NAT_1:12;
hence x in F by A5, A10, A11; :: thesis: verum

end;

suppose A13: x in {(m + (n + 1))} ; :: thesis: b₁ in F

then reconsider k = x as Element of NAT by TARSKI:def 1;
A14: x = m + (n + 1) by A13, TARSKI:def 1;
then m <= k by NAT_1:11;
hence x in F by A5, A14; :: thesis: verum

end;

end;

end;

then A15: F = { k where k is Nat : ( m <= k & k <= m + n ) } \/ {(m + (n + 1))} by TARSKI:2;
card F1 = n + 1 by A2;
hence card F = (n + 1) + 1 by A15, A4, CARD_2:41; :: thesis: verum

end;

end;

A16: S₁[ 0 ]

proof

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

now :: thesis: for x being object holds
( ( 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 ) )

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

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

assume x = m ; :: thesis: x in F
hence x in F by A17; :: thesis: verum

end;

then F = {m} by TARSKI:def 1;
hence card F = 0 + 1 by CARD_1:30; :: thesis: verum

end;

for n being Nat holds S₁[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