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 :: thesis: for x, y being Element of n -tuples_on D holds G . (x,y) = H . (x,y)

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 ; :: thesis: verum