reconsider n = n as non zero Nat by A1, TARSKI:1;
defpred S1[ Nat, Nat, 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]
proof
let k, l be Element of Segm n; :: thesis: ex c being Element of Segm n st S1[k,l,c]
(k + l) mod n < n by NAT_D:1;
then reconsider c = (k + l) mod n as Element of Segm n by NAT_1:44;
take c ; :: thesis: S1[k,l,c]
thus S1[k,l,c] ; :: thesis: verum
end;
ex o being BinOp of (Segm n) st
for a, b being Element of Segm n holds S1[a,b,o . (a,b)] 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 ; :: thesis: verum