deffunc H_{1}( Element of EC_SetAffCo (z,p), Element of EC_SetAffCo (z,p)) -> Element of ProjCo (GF p) = rep_pt ((addell_ProjCo (z,p)) . ($1,$2));

for o1, o2 being BinOp of (EC_SetAffCo (z,p)) st ( for P, Q being Element of EC_SetAffCo (z,p) holds o1 . (P,Q) = H_{1}(P,Q) ) & ( for P, Q being Element of EC_SetAffCo (z,p) holds o2 . (P,Q) = H_{1}(P,Q) ) holds

o1 = o2 from BINOP_2:sch 2();

hence for b_{1}, b_{2} being BinOp of (EC_SetAffCo (z,p)) st ( for P, Q being Element of EC_SetAffCo (z,p) holds b_{1} . (P,Q) = rep_pt ((addell_ProjCo (z,p)) . (P,Q)) ) & ( for P, Q being Element of EC_SetAffCo (z,p) holds b_{2} . (P,Q) = rep_pt ((addell_ProjCo (z,p)) . (P,Q)) ) holds

b_{1} = b_{2}
; :: thesis: verum

for o1, o2 being BinOp of (EC_SetAffCo (z,p)) st ( for P, Q being Element of EC_SetAffCo (z,p) holds o1 . (P,Q) = H

o1 = o2 from BINOP_2:sch 2();

hence for b

b