deffunc H₁( Point of M, Point of M) -> Element of (vectgroup M) = vector $1,$2;
consider f being Function of [:the carrier of M,the carrier of M:],the carrier of (vectgroup M) such that
A1: for p, q being Point of M holds f . p,q = H₁(p,q) from BINOP_1:sch 4();
take f ; :: thesis: for p, q being Point of M holds f . p,q = vect p,q
for p, q being Point of M holds f . p,q = vect p,q

proof

let p, q be Point of M; :: thesis: f . p,q = vect p,q
thus f . p,q = vector p,q by A1
.= vect p,q ; :: thesis: verum

end;

hence for p, q being Point of M holds f . p,q = vect p,q ; :: thesis: verum