deffunc H1( 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) = H1(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