deffunc H₁( Nat) -> set = meet { (B . k) where k is Element of NAT : $1 <= k } ;
thus ex f being Function st
( dom f = NAT & ( for n being Element of NAT holds f . n = H₁(n) ) ) from FUNCT_1:sch 4(); :: thesis: verum