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