let i1, i2 be BinOp of (Segm n); :: thesis: ( ( for k, l being Element of Segm n holds i1 . (k,l) = (k + l) mod n ) & ( for k, l being Element of Segm n holds i2 . (k,l) = (k + l) mod n ) implies i1 = i2 )
assume that
A3: for k, l being Element of Segm n holds i1 . (k,l) = (k + l) mod n and
A4: for k, l being Element of Segm n holds i2 . (k,l) = (k + l) mod n ; :: thesis: i1 = i2
for k, l being Element of Segm n holds i1 . (k,l) = i2 . (k,l)

proof

let k, l be Element of Segm n; :: thesis: i1 . (k,l) = i2 . (k,l)
thus i1 . (k,l) = (k + l) mod n by A3
.= i2 . (k,l) by A4 ; :: thesis: verum

end;

hence i1 = i2 by BINOP_1:2; :: thesis: verum