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 :: thesis: for x, y being Point of (TOP-REAL n) holds f . (x,y) = g . (x,y)
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