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 S1[ 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 S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
thus S1[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 b1 in F ) )
hereby :: thesis: ( x in F1 \/ {(m + (n + 1))} implies b1 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 ;
hence x in F1 \/ {(m + (n + 1))} by ; :: thesis: verum
end;
assume A9: x in F1 \/ {(m + (n + 1))} ; :: thesis: b1 in F
per cases ( x in F1 or x in {(m + (n + 1))} ) by ;
suppose x in F1 ; :: thesis: b1 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 ;
hence x in F by A5, A10, A11; :: thesis: verum
end;
suppose A13: x in {(m + (n + 1))} ; :: thesis: b1 in F
then reconsider k = x as Element of NAT by TARSKI:def 1;
A14: x = m + (n + 1) by ;
then m <= k by NAT_1:11;
hence x in F by ; :: 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 ; :: thesis: verum
end;
end;
A16: S1[ 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 S1[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