deffunc H₁( Nat) -> Nat = $1;
let m, n be Nat; :: thesis: card { k where k is Nat : ( m <= k & k <= m + n ) } = n + 1
defpred S₁[ Nat] means m <= $1;
set F = { H₁(k) where k is Nat : ( k <= m + n & S₁[k] ) } ;
{ H₁(k) where k is Nat : ( k <= m + n & S₁[k] ) } is finite from FINSEQ_1:sch 6();
then reconsider F = { H₁(k) where k is Nat : ( k <= m + n & S₁[k] ) } as finite set ;
F = { H₁(k) where k is Nat : ( m <= k & k <= m + n ) }

proof

thus F c= { H₁(k) where k is Nat : ( m <= k & k <= m + n ) } :: according to XBOOLE_0:def 10 :: thesis: { H₁(k) where k is Nat : ( m <= k & k <= m + n ) } c= F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in { H₁(k) where k is Nat : ( m <= k & k <= m + n ) } )
assume x in F ; :: thesis: x in { H₁(k) where k is Nat : ( m <= k & k <= m + n ) }
then ex k1 being Nat st
( x = H₁(k1) & k1 <= m + n & m <= k1 ) ;
then ex k1 being Nat st
( x = H₁(k1) & m <= k1 & k1 <= m + n ) ;
hence x in { H₁(k) where k is Nat : ( m <= k & k <= m + n ) } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₁(k) where k is Nat : ( m <= k & k <= m + n ) } or x in F )
assume x in { H₁(k) where k is Nat : ( m <= k & k <= m + n ) } ; :: thesis: x in F
then ex k1 being Nat st
( x = H₁(k1) & m <= k1 & k1 <= m + n ) ;
hence x in F ; :: thesis: verum

end;

then reconsider G = { H₁(k) where k is Nat : ( m <= k & k <= m + n ) } as finite set ;
card G = n + 1 by Lm1;
hence card { k where k is Nat : ( m <= k & k <= m + n ) } = n + 1 ; :: thesis: verum