let V be RealLinearSpace; for u, v, y being VECTOR of V holds u,v // y # u,y # v
let u, v, y be VECTOR of V; u,v // y # u,y # v
set p = y # u;
set r = y # v;
A1:
( y + u = (y # u) + (y # u) & y + v = (y # v) + (y # v) )
by Def2;
2 * ((y # v) - (y # u)) =
((1 + 1) * (y # v)) - ((1 + 1) * (y # u))
by RLVECT_1:34
.=
((1 * (y # v)) + (1 * (y # v))) - ((1 + 1) * (y # u))
by RLVECT_1:def 6
.=
((1 * (y # v)) + (1 * (y # v))) - ((1 * (y # u)) + (1 * (y # u)))
by RLVECT_1:def 6
.=
((y # v) + (1 * (y # v))) - ((1 * (y # u)) + (1 * (y # u)))
by RLVECT_1:def 8
.=
((y # v) + (y # v)) - ((1 * (y # u)) + (1 * (y # u)))
by RLVECT_1:def 8
.=
((y # v) + (y # v)) - ((y # u) + (1 * (y # u)))
by RLVECT_1:def 8
.=
(y + v) - (y + u)
by A1, RLVECT_1:def 8
.=
v + (y - (y + u))
by RLVECT_1:def 3
.=
v + ((y - y) - u)
by RLVECT_1:27
.=
v + ((0. V) - u)
by RLVECT_1:15
.=
v - u
by RLVECT_1:14
.=
1 * (v - u)
by RLVECT_1:def 8
;
hence
u,v // y # u,y # v
by ANALOAF:def 1; verum