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