let V be RealLinearSpace; :: thesis: for u1, u2, v1, v2 being VECTOR of V st u1 # u2 = v1 # v2 holds
v1 - u1 = - (v2 - u2)
let u1, u2, v1, v2 be VECTOR of V; :: thesis: ( u1 # u2 = v1 # v2 implies v1 - u1 = - (v2 - u2) )
set p = u1 # u2;
A1: (u1 # u2) + (u1 # u2) = u1 + u2 by Def2;
assume u1 # u2 = v1 # v2 ; :: thesis: v1 - u1 = - (v2 - u2)
then A2: (u1 # u2) + (u1 # u2) = v1 + v2 by Def2;
(v1 - u1) + v2 = (v2 + v1) - u1 by RLVECT_1:def 3
.= u2 by A1, A2, RLSUB_2:61 ;
then (v1 - u1) + (v2 - u2) = u2 - u2 by RLVECT_1:def 3
.= 0. V by RLVECT_1:15 ;
hence v1 - u1 = - (v2 - u2) by RLVECT_1:6; :: thesis: verum