deffunc H₁( Element of A) -> set = (card (X /\ (Class the InternalRel of A,$1))) / (card (Class the InternalRel of A,$1));
A3: for A1, A2 being Function of the carrier of A,REAL st ( for x being Element of A holds A1 . x = H₁(x) ) & ( for x being Element of A holds A2 . x = H₁(x) ) holds
A1 = A2 from BINOP_2:sch 1();
let A1, A2 be Function of the carrier of A,REAL ; :: thesis: ( ( for x being Element of A holds A1 . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x)) ) & ( for x being Element of A holds A2 . x = (card (X /\ (Class the InternalRel of A,x))) / (card (Class the InternalRel of A,x)) ) implies A1 = A2 )
assume ( ( for x being Element of A holds A1 . x = H₁(x) ) & ( for x being Element of A holds A2 . x = H₁(x) ) ) ; :: thesis: A1 = A2
hence A1 = A2 by A3; :: thesis: verum