deffunc H_{1}( 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_{1}(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)

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

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

hence
for p, q being Point of M holds f . (p,q) = vect (p,q)
; :: thesis: verum
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;thus f . (p,q) = vector (p,q) by A1

.= vect (p,q) ; :: thesis: verum