reconsider n = n as natural non zero Number by A1;

deffunc H_{1}( Element of Segm n, Element of Segm n) -> set = ($1 * $2) mod n;

for o1, o2 being BinOp of (Segm n) st ( for a, b being Element of Segm n holds o1 . (a,b) = H_{1}(a,b) ) & ( for a, b being Element of Segm n holds o2 . (a,b) = H_{1}(a,b) ) holds

o1 = o2 from BINOP_2:sch 2();

hence for b_{1}, b_{2} being BinOp of (Segm n) st ( for k, l being Element of Segm n holds b_{1} . (k,l) = (k * l) mod n ) & ( for k, l being Element of Segm n holds b_{2} . (k,l) = (k * l) mod n ) holds

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

deffunc H

for o1, o2 being BinOp of (Segm n) st ( for a, b being Element of Segm n holds o1 . (a,b) = H

o1 = o2 from BINOP_2:sch 2();

hence for b

b