deffunc H₁( set ) -> set = card (f . $1);
thus ex g being Cardinal-Function st
( dom g = dom f & ( for x being set st x in dom f holds
g . x = H₁(x) ) ) from CARD_3:sch 1(); :: thesis: verum