let f, g be Function of [:(TOP-REAL n),(TOP-REAL n):],(TOP-REAL n); :: thesis: ( ( for x, y being Point of (TOP-REAL n) holds f . x,y = x (#) y ) & ( for x, y being Point of (TOP-REAL n) holds g . x,y = x (#) y ) implies f = g )
assume that
A2: for x, y being Point of (TOP-REAL n) holds f . x,y = x (#) y and
A3: for x, y being Point of (TOP-REAL n) holds g . x,y = x (#) y ; :: thesis: f = g

now

let x, y be Point of (TOP-REAL n); :: thesis: f . x,y = g . x,y
thus f . x,y = x (#) y by A2
.= g . x,y by A3 ; :: thesis: verum

end;

hence f = g by A1, BINOP_1:2; :: thesis: verum