reconsider n = n as non zero Nat by A1, TARSKI:1;
defpred S₁[ 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 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]
(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: S₁[k,l,c]
thus S₁[k,l,c] ; :: thesis: verum

end;

ex o being BinOp of (Segm n) st
for a, b being Element of Segm n holds S₁[a,b,o . (a,b)] 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