let S1, S2 be BinOp of the carrier of F; :: thesis:
assume that
A3: for x, y being Element of F holds S1 . (x,y) = the addF of F . (x,((comp F) . y)) and
A4: for x, y being Element of F holds S2 . (x,y) = the addF of F . (x,((comp F) . y)) ; :: thesis:

let p be object ; :: thesis:
assume p in [: the carrier of F, the carrier of F:] ; :: thesis:
then consider x, y being object such that
A5: ( x in the carrier of F & y in the carrier of F ) and
A6: p = [x,y] by ZFMISC_1:def 2;
thus S1 . p = S1 . (x,y) by A6
.= the addF of F . (x,((comp F) . y)) by A3, A5
.= S2 . (x,y) by A4, A5
.= S2 . p by A6 ; :: thesis:

end;