deffunc H_{1}( Nat) -> Nat = $1;

let m, n be Nat; :: thesis: card { k where k is Nat : ( m <= k & k <= m + n ) } = n + 1

defpred S_{1}[ Nat] means m <= $1;

set F = { H_{1}(k) where k is Nat : ( k <= m + n & S_{1}[k] ) } ;

{ H_{1}(k) where k is Nat : ( k <= m + n & S_{1}[k] ) } is finite
from FINSEQ_1:sch 6();

then reconsider F = { H_{1}(k) where k is Nat : ( k <= m + n & S_{1}[k] ) } as finite set ;

F = { H_{1}(k) where k is Nat : ( m <= k & k <= m + n ) }
_{1}(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

let m, n be Nat; :: thesis: card { k where k is Nat : ( m <= k & k <= m + n ) } = n + 1

defpred S

set F = { H

{ H

then reconsider F = { H

F = { H

proof

then reconsider G = { H
thus
F c= { H_{1}(k) where k is Nat : ( m <= k & k <= m + n ) }
:: according to XBOOLE_0:def 10 :: thesis: { H_{1}(k) where k is Nat : ( m <= k & k <= m + n ) } c= F_{1}(k) where k is Nat : ( m <= k & k <= m + n ) } or x in F )

assume x in { H_{1}(k) where k is Nat : ( m <= k & k <= m + n ) }
; :: thesis: x in F

then ex k1 being Nat st

( x = H_{1}(k1) & m <= k1 & k1 <= m + n )
;

hence x in F ; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in { H_{1}(k) where k is Nat : ( m <= k & k <= m + n ) } )

assume x in F ; :: thesis: x in { H_{1}(k) where k is Nat : ( m <= k & k <= m + n ) }

then ex k1 being Nat st

( x = H_{1}(k1) & k1 <= m + n & m <= k1 )
;

then ex k1 being Nat st

( x = H_{1}(k1) & m <= k1 & k1 <= m + n )
;

hence x in { H_{1}(k) where k is Nat : ( m <= k & k <= m + n ) }
; :: thesis: verum

end;assume x in F ; :: thesis: x in { H

then ex k1 being Nat st

( x = H

then ex k1 being Nat st

( x = H

hence x in { H

assume x in { H

then ex k1 being Nat st

( x = H

hence x in F ; :: thesis: verum

card G = n + 1 by Lm1;

hence card { k where k is Nat : ( m <= k & k <= m + n ) } = n + 1 ; :: thesis: verum