reconsider n = n as non zero Nat by A1, TARSKI:1;
defpred S1[ Element of Segm n, Element of Segm n, set ] means $3 = ($1 * $2) mod n;
A2:
for k, l being Element of Segm n ex c being Element of Segm n st S1[k,l,c]
ex c being BinOp of (Segm n) st
for k, l being Element of Segm n holds S1[k,l,c . (k,l)]
from BINOP_1:sch 3(A2);
hence
ex b1 being BinOp of (Segm n) st
for k, l being Element of Segm n holds b1 . (k,l) = (k * l) mod n
; verum