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

per cases ( u = v or u1 = v1 or ( u <> v & u1 <> v1 ) ) ;

suppose u = v ; :: thesis: u,v '||' u # v1,v # u1

then u,v // u # v1,v # u1 by ANALOAF:9;
hence u,v '||' u # v1,v # u1 ; :: thesis: verum

end;

suppose u1 = v1 ; :: thesis: u,v '||' u # v1,v # u1

then u,v // u # v1,v # u1 by Th8;
hence u,v '||' u # v1,v # u1 ; :: thesis: verum

end;

suppose ( u <> v & u1 <> v1 ) ; :: thesis: u,v '||' u # v1,v # u1

then consider a, b being Real such that
0 < a and
A2: 0 < b and
A3: a * (v - u) = b * (v1 - u1) by A1, ANALOAF:def 1;
A4: b * (u1 - v1) = b * (- (v1 - u1)) by RLVECT_1:33
.= - (a * (v - u)) by A3, RLVECT_1:25
.= a * (- (v - u)) by RLVECT_1:25
.= (- a) * (v - u) by RLVECT_1:24 ;
set p = u # v1;
set q = v # u1;
set A = b * 2;
set D = b - a;
A5: b * 2 <> 0 by A2;
(b * 2) * ((v # u1) - (u # v1)) = b * (2 * ((v # u1) - (u # v1))) by RLVECT_1:def 7
.= b * (((1 + 1) * (v # u1)) - (2 * (u # v1))) by RLVECT_1:34
.= b * (((1 * (v # u1)) + (1 * (v # u1))) - (2 * (u # v1))) by RLVECT_1:def 6
.= b * (((v # u1) + (1 * (v # u1))) - (2 * (u # v1))) by RLVECT_1:def 8
.= b * (((v # u1) + (v # u1)) - (2 * (u # v1))) by RLVECT_1:def 8
.= b * ((v + u1) - (2 * (u # v1))) by Def2
.= b * (v + (u1 - ((1 + 1) * (u # v1)))) by RLVECT_1:def 3
.= b * (v + (u1 - ((1 * (u # v1)) + (1 * (u # v1))))) by RLVECT_1:def 6
.= b * (v + (u1 - ((u # v1) + (1 * (u # v1))))) by RLVECT_1:def 8
.= b * (v + (u1 - ((u # v1) + (u # v1)))) by RLVECT_1:def 8
.= b * (v + (u1 - (u + v1))) by Def2
.= b * (v + ((u1 - v1) - u)) by RLVECT_1:27
.= b * ((v + (u1 - v1)) - u) by RLVECT_1:def 3
.= b * ((u1 - v1) + (v - u)) by RLVECT_1:def 3
.= ((- a) * (v - u)) + (b * (v - u)) by A4, RLVECT_1:def 5
.= (b + (- a)) * (v - u) by RLVECT_1:def 6
.= (b - a) * (v - u) ;
then ( u,v // u # v1,v # u1 or u,v // v # u1,u # v1 ) by A5, ANALMETR:14;
hence u,v '||' u # v1,v # u1 ; :: thesis: verum

end;

end;