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