deffunc H₁( set ) -> set = (card (X /\ (Class the InternalRel of A,$1))) / (card (Class the InternalRel of A,$1));
A1: for x being set st x in the carrier of A holds
H₁(x) in REAL by XREAL_0:def 1;
ex f being Function of the carrier of A,REAL st
for x being set st x in the carrier of A holds
f . x = H₁(x) from FUNCT_2:sch 2(A1);
then consider f being Function of the carrier of A,REAL such that
A2: for x being set st x in the carrier of A holds
f . x = H₁(x) ;
take f ; :: thesis: for x being Element of A holds f . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x))
let x be Element of A; :: thesis: f . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x))
thus f . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x)) by A2; :: thesis: verum