deffunc H₁( object ) -> set = card (Im (O,$1));
consider f being Function such that
A1: ( dom f = X & ( for x being object st x in X holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
rng f c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in NAT )
assume y in rng f ; :: thesis: y in NAT
then consider x being object such that
A2: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
reconsider x = x as Element of X by A1, A2;
y = card (x . O) by A1, A2;
hence y in NAT ; :: thesis: verum

end;

then reconsider f = f as Function of X,NAT by A1, FUNCT_2:2;
take f ; :: thesis: for x being Element of X holds f . x = card (x . O)
let x be Element of X; :: thesis: f . x = card (x . O)

per cases ( X = {} or X <> {} ) ;

suppose X = {} ; :: thesis: f . x = card (x . O)

then ( f . x = 0 & x . O = {} ) by A1, FUNCT_1:def 2;
hence f . x = card (x . O) ; :: thesis: verum

end;

suppose X <> {} ; :: thesis: f . x = card (x . O)

hence f . x = card (x . O) by A1; :: thesis: verum

end;

end;