let V be RealLinearSpace; :: thesis: for u, v, u1, v1 being VECTOR of V st u,v // u1,v1 holds
u,v // u # u1,v # v1
let u, v, u1, v1 be VECTOR of V; :: thesis: ( u,v // u1,v1 implies u,v // u # u1,v # v1 )
assume A1: u,v // u1,v1 ; :: thesis: u,v // u # u1,v # v1

now

assume ( u <> v & u1 <> v1 ) ; :: thesis: u,v // u # u1,v # v1
then consider a, b being Real such that
A2: ( 0 < a & 0 < b & a * (v - u) = b * (v1 - u1) ) by A1, ANALOAF:def 1;
set p = u # u1;
set q = v # v1;
A3: 0 < a + b by A2, XREAL_1:36;
A4: 0 < b * 2 by A2, XREAL_1:131;
(b * 2) * ((v # v1) - (u # u1)) = b * (2 * ((v # v1) - (u # u1))) by RLVECT_1:def 9
.= b * (((1 + 1) * (v # v1)) - (2 * (u # u1))) by RLVECT_1:48
.= b * (((1 * (v # v1)) + (1 * (v # v1))) - (2 * (u # u1))) by RLVECT_1:def 9
.= b * (((v # v1) + (1 * (v # v1))) - (2 * (u # u1))) by RLVECT_1:def 9
.= b * (((v # v1) + (v # v1)) - (2 * (u # u1))) by RLVECT_1:def 9
.= b * ((v + v1) - (2 * (u # u1))) by Def2
.= b * (v + (v1 - ((1 + 1) * (u # u1)))) by RLVECT_1:def 6
.= b * (v + (v1 - ((1 * (u # u1)) + (1 * (u # u1))))) by RLVECT_1:def 9
.= b * (v + (v1 - ((u # u1) + (1 * (u # u1))))) by RLVECT_1:def 9
.= b * (v + (v1 - ((u # u1) + (u # u1)))) by RLVECT_1:def 9
.= b * (v + (v1 - (u + u1))) by Def2
.= b * (v + ((v1 - u1) - u)) by RLVECT_1:41
.= b * ((v + (v1 - u1)) - u) by RLVECT_1:def 6
.= b * ((v1 - u1) + (v - u)) by RLVECT_1:def 6
.= (a * (v - u)) + (b * (v - u)) by A2, RLVECT_1:def 9
.= (a + b) * (v - u) by RLVECT_1:def 9 ;
hence u,v // u # u1,v # v1 by A3, A4, ANALOAF:def 1; :: thesis: verum

end;

hence u,v // u # u1,v # v1 by Th10, ANALOAF:18; :: thesis: verum