deffunc H1( Nat) -> Nat = \$1;
let m, n be Nat; :: thesis: card { k where k is Nat : ( m <= k & k <= m + n ) } = n + 1
defpred S1[ Nat] means m <= \$1;
set F = { H1(k) where k is Nat : ( k <= m + n & S1[k] ) } ;
{ H1(k) where k is Nat : ( k <= m + n & S1[k] ) } is finite from then reconsider F = { H1(k) where k is Nat : ( k <= m + n & S1[k] ) } as finite set ;
F = { H1(k) where k is Nat : ( m <= k & k <= m + n ) }
proof
thus F c= { H1(k) where k is Nat : ( m <= k & k <= m + n ) } :: according to XBOOLE_0:def 10 :: thesis: { H1(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 { H1(k) where k is Nat : ( m <= k & k <= m + n ) } )
assume x in F ; :: thesis: x in { H1(k) where k is Nat : ( m <= k & k <= m + n ) }
then ex k1 being Nat st
( x = H1(k1) & k1 <= m + n & m <= k1 ) ;
then ex k1 being Nat st
( x = H1(k1) & m <= k1 & k1 <= m + n ) ;
hence x in { H1(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 { H1(k) where k is Nat : ( m <= k & k <= m + n ) } or x in F )
assume x in { H1(k) where k is Nat : ( m <= k & k <= m + n ) } ; :: thesis: x in F
then ex k1 being Nat st
( x = H1(k1) & m <= k1 & k1 <= m + n ) ;
hence x in F ; :: thesis: verum
end;
then reconsider G = { H1(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