reconsider n = n as non zero natural number by A1;
defpred S₁[ 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₁[k,l,c]

proof

let k, l be Element of Segm n; :: thesis: ex c being Element of Segm n st S₁[k,l,c]
reconsider k' = k, l' = l as Element of NAT ;
(k' * l') mod n < n by NAT_D:1;
then reconsider c = (k' * l') mod n as Element of Segm n by GR_CY_1:10;
take c ; :: thesis: S₁[k,l,c]
thus S₁[k,l,c] ; :: thesis: verum

end;

ex c being BinOp of (Segm n) st
for k, l being Element of Segm n holds S₁[k,l,c . k,l] from BINOP_1:sch 3(A2);
hence ex b₁ being BinOp of (Segm n) st
for k, l being Element of Segm n holds b₁ . k,l = (k * l) mod n ; :: thesis: verum