deffunc H₁( object ) -> set = {$1};

A1: now :: thesis: for x being object st x in A holds
H₁(x) in Fin A

let x be object ; :: thesis: ( x in A implies H₁(x) in Fin A )
assume A2: x in A ; :: thesis: H₁(x) in Fin A
then reconsider A9 = A as non empty set ;
reconsider x9 = x as Element of A9 by A2;
{.x9.} in Fin A9 ;
hence H₁(x) in Fin A ; :: thesis: verum

end;

thus ex f being Function of A,(Fin A) st
for x being object st x in A holds
f . x = H₁(x) from FUNCT_2:sch 2(A1); :: thesis: verum