let f, g be Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M); ( ( for p, q being Point of M holds f . (p,q) = vect (p,q) ) & ( for p, q being Point of M holds g . (p,q) = vect (p,q) ) implies f = g )
assume that
A2:
for p, q being Point of M holds f . (p,q) = vect (p,q)
and
A3:
for p, q being Point of M holds g . (p,q) = vect (p,q)
; f = g
for p, q being Point of M holds f . (p,q) = g . (p,q)
proof
let p,
q be
Point of
M;
f . (p,q) = g . (p,q)
thus f . (
p,
q) =
vect (
p,
q)
by A2
.=
g . (
p,
q)
by A3
;
verum
end;
hence
f = g
by BINOP_1:2; verum