deffunc H₂( type of s) -> Element of omega = card (dom (repr_of $1));
thus ex S being Function of the carrier of s,NAT st
for x being type of s holds S . x = H₂(x) from FUNCT_2:sch 4(); :: thesis: verum