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
A3: for p, q being Point of M holds f . p,q = vect p,q and
A4: 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

let p, q be Point of M; :: thesis: f . p,q = g . p,q
thus f . p,q = vect p,q by A3
.= g . p,q by A4 ; :: thesis: verum

end;

hence f = g by BINOP_1:2; :: thesis: verum