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: 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 A2: 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 consider k being Element of NAT such that
A3: ( x = k & m <= k & k <= m + 0 ) by A2;
thus x = m by A3, XXREAL_0:1; :: thesis: verum

end;

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

end;

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

end;

A4: now

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

proof

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 )
assume A6: F = { k where k is Element of NAT : ( m <= k & k <= m + (n + 1) ) } ; :: thesis: card F = (n + 1) + 1
set F1 = { k where k is Element of NAT : ( m <= k & k <= m + n ) } ;
reconsider F2 = { k where k is Element of NAT : k <= m + n } as finite set by CQC_THE1:12;
{ 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 consider k being Element of NAT such that
A7: ( x = k & m <= k & k <= m + n ) ;
thus x in F2 by A7; :: thesis: verum

end;

then reconsider F1 = { k where k is Element of NAT : ( m <= k & k <= m + n ) } as finite set ;

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
A8: ( x = k & m <= k & k <= m + (n + 1) ) by A6;
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 A8, TARSKI:def 1;
hence x in F1 \/ {(m + (n + 1))} by A8, 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 Element of NAT such that
A10: ( x = k & m <= k & k <= m + n ) ;
k <= (m + n) + 1 by A10, NAT_1:12;
hence x in F by A6, A10; :: thesis: verum

end;

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

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

end;

end;

end;

then A13: F = { k where k is Element of NAT : ( m <= k & k <= m + n ) } \/ {(m + (n + 1))} by TARSKI:2;
A14: 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 consider k being Element of NAT such that
A15: ( m + (n + 1) = k & m <= k & k <= m + n ) ;
(m + n) + 1 <= (m + n) + 0 by A15;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

card F1 = n + 1 by A5;
hence card F = (n + 1) + 1 by A13, A14, CARD_2:54; :: thesis: verum

end;

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A4);
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