reconsider n = n as non zero Nat by A1, TARSKI:1;

defpred S_{1}[ 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 S_{1}[k,l,c]

for k, l being Element of Segm n holds S_{1}[k,l,c . (k,l)]
from BINOP_1:sch 3(A2);

hence ex b_{1} being BinOp of (Segm n) st

for k, l being Element of Segm n holds b_{1} . (k,l) = (k * l) mod n
; :: thesis: verum

defpred S

A2: for k, l being Element of Segm n ex c being Element of Segm n st S

proof

ex c being BinOp of (Segm n) st
let k, l be Element of Segm n; :: thesis: ex c being Element of Segm n st S_{1}[k,l,c]

reconsider k9 = k, l9 = l as Element of NAT ;

(k9 * l9) mod n < n by NAT_D:1;

then reconsider c = (k9 * l9) mod n as Element of Segm n by NAT_1:44;

take c ; :: thesis: S_{1}[k,l,c]

thus S_{1}[k,l,c]
; :: thesis: verum

end;reconsider k9 = k, l9 = l as Element of NAT ;

(k9 * l9) mod n < n by NAT_D:1;

then reconsider c = (k9 * l9) mod n as Element of Segm n by NAT_1:44;

take c ; :: thesis: S

thus S

for k, l being Element of Segm n holds S

hence ex b

for k, l being Element of Segm n holds b