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