let f, g be Function of [:R^1,R^1:],R^1; :: thesis: ( ( for x, y being Point of R^1 holds f . (x,y) = x * y ) & ( for x, y being Point of R^1 holds g . (x,y) = x * y ) implies f = g )
assume that
A2: for x, y being Point of R^1 holds f . (x,y) = x * y and
A3: for x, y being Point of R^1 holds g . (x,y) = x * y ; :: thesis: f = g

now :: thesis: for x, y being Point of R^1 holds f . (x,y) = g . (x,y)

let x, y be Point of R^1; :: 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 Lm1, BINOP_1:2; :: thesis: verum