let m be Element of NAT ; :: thesis: for n being Element of NAT
for F being finite set st F = { k where k is Element of NAT : ( m <= k & k <= m + n ) } holds
card F = n + 1
defpred S₁[ Element of NAT ] means for F being finite set st F = { k where k is Element of NAT : ( m <= k & k <= m + $1 ) } holds
card F = $1 + 1;

A1: now

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

proof

reconsider F2 = { k where k is Element of NAT : k <= m + n } as finite set by CQC_THE1:12;
set F1 = { k where k is Element of NAT : ( m <= k & k <= m + n ) } ;
{ k where k is Element of NAT : ( m <= k & k <= m + n ) } c= F2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( m <= k & k <= m + n ) } or x in F2 )
assume x in { k where k is Element of NAT : ( m <= k & k <= m + n ) } ; :: thesis: x in F2
then ex k being Element of NAT st
( x = k & m <= k & k <= m + n ) ;
hence x in F2 ; :: thesis: verum

end;

then reconsider F1 = { k where k is Element of NAT : ( m <= k & k <= m + n ) } as finite set ;
let F be finite set ; :: thesis: ( F = { k where k is Element of NAT : ( m <= k & k <= m + (n + 1) ) } implies card F = (n + 1) + 1 )
A3: not m + (n + 1) in { k where k is Element of NAT : ( m <= k & k <= m + n ) }

proof

assume m + (n + 1) in { k where k is Element of NAT : ( m <= k & k <= m + n ) } ; :: thesis: contradiction
then ex k being Element of NAT st
( m + (n + 1) = k & m <= k & k <= m + n ) ;
then (m + n) + 1 <= (m + n) + 0 ;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

assume A4: F = { k where k is Element of NAT : ( m <= k & k <= m + (n + 1) ) } ; :: thesis: card F = (n + 1) + 1

now

let x be set ; :: 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 Element of NAT such that
A5: x = k and
A6: m <= k and
A7: k <= m + (n + 1) by A4;
k <= (m + n) + 1 by A7;
then ( k <= m + n or k = m + (n + 1) ) by NAT_1:8;
then ( k in F1 or k in {(m + (n + 1))} ) by A6, TARSKI:def 1;
hence x in F1 \/ {(m + (n + 1))} by A5, XBOOLE_0:def 3; :: thesis: verum

end;

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

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

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

then consider k being Element of NAT such that
A9: x = k and
A10: m <= k and
A11: k <= m + n ;
k <= (m + n) + 1 by A11, NAT_1:12;
hence x in F by A4, A9, A10; :: thesis: verum

end;

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

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

end;

end;

end;

then A14: F = { k where k is Element of 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 A14, A3, CARD_2:54; :: thesis: verum

end;

end;

A15: S₁[ 0 ]

proof

let F be finite set ; :: thesis: ( F = { k where k is Element of NAT : ( m <= k & k <= m + 0 ) } implies card F = 0 + 1 )
assume A16: F = { k where k is Element of NAT : ( m <= k & k <= m + 0 ) } ; :: thesis: card F = 0 + 1

now

let x be set ; :: 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 Element of NAT st
( x = k & m <= k & k <= m + 0 ) by A16;
hence x = m by XXREAL_0:1; :: thesis: verum

end;

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

end;

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

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A15, A1);
hence for n being Element of NAT
for F being finite set st F = { k where k is Element of NAT : ( m <= k & k <= m + n ) } holds
card F = n + 1 ; :: thesis: verum