let V be RealLinearSpace; :: thesis: for u, v, u1, v1 being VECTOR of V st u,v // u1,v1 holds
u,v '||' u # v1,v # u1
let u, v, u1, 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

A2: now

assume u = v ; :: thesis: u,v '||' u # v1,v # u1
then u,v // u # v1,v # u1 by ANALOAF:18;
hence u,v '||' u # v1,v # u1 by Def1; :: thesis: verum

end;

A3: now

assume u1 = v1 ; :: thesis: u,v '||' u # v1,v # u1
then u,v // u # v1,v # u1 by Th10;
hence u,v '||' u # v1,v # u1 by Def1; :: thesis: verum

end;

now

assume ( u <> v & u1 <> v1 ) ; :: thesis: u,v '||' u # v1,v # u1
then consider a, b being Real such that
A4: ( 0 < a & 0 < b & a * (v - u) = b * (v1 - u1) ) by A1, ANALOAF:def 1;
set p = u # v1;
set q = v # u1;
set A = b * 2;
set D = b - a;
A5: (b * 2) * ((v # u1) - (u # v1)) = (b - a) * (v - u)

proof

A6: b * (u1 - v1) = b * (- (v1 - u1)) by RLVECT_1:47
.= - (a * (v - u)) by A4, RLVECT_1:39
.= a * (- (v - u)) by RLVECT_1:39
.= (- a) * (v - u) by RLVECT_1:38 ;
thus (b * 2) * ((v # u1) - (u # v1)) = b * (2 * ((v # u1) - (u # v1))) by RLVECT_1:def 9
.= b * (((1 + 1) * (v # u1)) - (2 * (u # v1))) by RLVECT_1:48
.= b * (((1 * (v # u1)) + (1 * (v # u1))) - (2 * (u # v1))) by RLVECT_1:def 9
.= b * (((v # u1) + (1 * (v # u1))) - (2 * (u # v1))) by RLVECT_1:def 9
.= b * (((v # u1) + (v # u1)) - (2 * (u # v1))) by RLVECT_1:def 9
.= b * ((v + u1) - (2 * (u # v1))) by Def2
.= b * (v + (u1 - ((1 + 1) * (u # v1)))) by RLVECT_1:def 6
.= b * (v + (u1 - ((1 * (u # v1)) + (1 * (u # v1))))) by RLVECT_1:def 9
.= b * (v + (u1 - ((u # v1) + (1 * (u # v1))))) by RLVECT_1:def 9
.= b * (v + (u1 - ((u # v1) + (u # v1)))) by RLVECT_1:def 9
.= b * (v + (u1 - (u + v1))) by Def2
.= b * (v + ((u1 - v1) - u)) by RLVECT_1:41
.= b * ((v + (u1 - v1)) - u) by RLVECT_1:def 6
.= b * ((u1 - v1) + (v - u)) by RLVECT_1:def 6
.= ((- a) * (v - u)) + (b * (v - u)) by A6, RLVECT_1:def 9
.= (b + (- a)) * (v - u) by RLVECT_1:def 9
.= (b - a) * (v - u) ; :: thesis: verum

end;

b * 2 <> 0 by A4;
then ( u,v // u # v1,v # u1 or u,v // v # u1,u # v1 ) by A5, ANALMETR:18;
hence u,v '||' u # v1,v # u1 by Def1; :: thesis: verum

end;

hence u,v '||' u # v1,v # u1 by A2, A3; :: thesis: verum