let f, g be Function of [: the carrier of M, the carrier of M:], the carrier of (vectgroup M); :: thesis: ( ( 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) ; :: thesis: f = g

for p, q being Point of M holds f . (p,q) = g . (p,q)

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) ; :: thesis: f = g

for p, q being Point of M holds f . (p,q) = g . (p,q)

proof

hence
f = g
by BINOP_1:2; :: thesis: verum
let p, q be Point of M; :: thesis: f . (p,q) = g . (p,q)

thus f . (p,q) = vect (p,q) by A2

.= g . (p,q) by A3 ; :: thesis: verum

end;thus f . (p,q) = vect (p,q) by A2

.= g . (p,q) by A3 ; :: thesis: verum