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

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)

hence
f = g
by Lm1, BINOP_1:2; :: thesis: verumlet 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;thus f . (x,y) = x * y by A2

.= g . (x,y) by A3 ; :: thesis: verum