let G, H be BinOp of (n -tuples_on D); :: thesis: ( ( for x, y being Element of n -tuples_on D holds G . x,y = F .: x,y ) & ( for x, y being Element of n -tuples_on D holds H . x,y = F .: x,y ) implies G = H )
assume that
A3: for x, y being Element of n -tuples_on D holds G . x,y = F .: x,y and
A4: for x, y being Element of n -tuples_on D holds H . x,y = F .: x,y ; :: thesis: G = H

now

let x, y be Element of n -tuples_on D; :: thesis: G . x,y = H . x,y
G . x,y = F .: x,y by A3;
hence G . x,y = H . x,y by A4; :: thesis: verum

end;

hence G = H by BINOP_1:2; :: thesis: verum