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 finitefromFINSEQ_1:sch 6(); then reconsider F = { H1(k) where k is Nat : ( k <= m + n & S1[k] ) } as finiteset ;
F = { H1(k) where k is Nat : ( m <= k & k <= m + n ) }
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