let f, g be Function of [:R^1,R^1:],R^1; ( ( 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
; f = g
now for x, y being Point of R^1 holds f . (x,y) = g . (x,y)let x,
y be
Point of
R^1;
f . (x,y) = g . (x,y)thus f . (
x,
y) =
x * y
by A2
.=
g . (
x,
y)
by A3
;
verum end;
hence
f = g
by Lm1, BINOP_1:2; verum