let V be RealLinearSpace; :: thesis: for o, u, v, u1, v1 being VECTOR of V
for r being Real st o - u = r * (u1 - o) & r <> 0 & o,v '||' o,v1 & not o,u '||' o,v & u,v '||' u1,v1 holds
( v1 = u1 + (((- r) " ) * (v - u)) & v1 = o + (((- r) " ) * (v - o)) & v - u = (- r) * (v1 - u1) )
let o, u, v, u1, v1 be VECTOR of V; :: thesis: for r being Real st o - u = r * (u1 - o) & r <> 0 & o,v '||' o,v1 & not o,u '||' o,v & u,v '||' u1,v1 holds
( v1 = u1 + (((- r) " ) * (v - u)) & v1 = o + (((- r) " ) * (v - o)) & v - u = (- r) * (v1 - u1) )
let r be Real; :: thesis: ( o - u = r * (u1 - o) & r <> 0 & o,v '||' o,v1 & not o,u '||' o,v & u,v '||' u1,v1 implies ( v1 = u1 + (((- r) " ) * (v - u)) & v1 = o + (((- r) " ) * (v - o)) & v - u = (- r) * (v1 - u1) ) )
assume that
A1: ( o - u = r * (u1 - o) & r <> 0 ) and
A2: o,v '||' o,v1 and
A3: not o,u '||' o,v and
X: u,v '||' u1,v1 ; :: thesis: ( v1 = u1 + (((- r) " ) * (v - u)) & v1 = o + (((- r) " ) * (v - o)) & v - u = (- r) * (v1 - u1) )
set w = u1 + (((- r) " ) * (v - u));
A4: - r <> 0 by A1;
B6: 1 * (u - o) = (- r) * (u1 - o)

proof

1 * (u - o) = (- 1) * (- (u - o)) by RLVECT_1:40
.= (- 1) * (r * (u1 - o)) by A1, RLVECT_1:47
.= ((- 1) * r) * (u1 - o) by RLVECT_1:def 9
.= (- r) * (u1 - o) ;
hence 1 * (u - o) = (- r) * (u1 - o) ; :: thesis: verum

end;

B7: o,u '||' o,u1

proof

( o,u // o,u1 or o,u // u1,o ) by B6, ANALMETR:18;
hence o,u '||' o,u1 by GEOMTRAP:def 1; :: thesis: verum

end;

B8: 1 * (v - u) = (- r) * ((u1 + (((- r) " ) * (v - u))) - u1)

proof

(- r) * ((u1 + (((- r) " ) * (v - u))) - u1) = (- r) * (((- r) " ) * (v - u)) by RLSUB_2:78
.= ((- r) * ((- r) " )) * (v - u) by RLVECT_1:def 9
.= 1 * (v - u) by A4, XCMPLX_0:def 7 ;
hence 1 * (v - u) = (- r) * ((u1 + (((- r) " ) * (v - u))) - u1) ; :: thesis: verum

end;

then A5: v - u = (- r) * ((u1 + (((- r) " ) * (v - u))) - u1) by RLVECT_1:def 9;
B10: u,v '||' u1,u1 + (((- r) " ) * (v - u))

proof

( u,v // u1,u1 + (((- r) " ) * (v - u)) or u,v // u1 + (((- r) " ) * (v - u)),u1 ) by B8, ANALMETR:18;
hence u,v '||' u1,u1 + (((- r) " ) * (v - u)) by GEOMTRAP:def 1; :: thesis: verum

end;

A6: 1 * (o - v) = (- r) * (o - (u1 + (((- r) " ) * (v - u))))

proof

(- r) * (o - (u1 + (((- r) " ) * (v - u)))) = ((- r) * o) - ((- r) * (u1 + (((- r) " ) * (v - u)))) by RLVECT_1:48
.= ((- r) * o) - (((- r) * u1) + ((- r) * (((- r) " ) * (v - u)))) by RLVECT_1:def 9
.= ((- r) * o) - (((- r) * u1) + (((- r) * ((- r) " )) * (v - u))) by RLVECT_1:def 9
.= ((- r) * o) - (((- r) * u1) + (1 * (v - u))) by A4, XCMPLX_0:def 7
.= ((- r) * o) - (((- r) * u1) + (v - u)) by RLVECT_1:def 9
.= (((- r) * o) - ((- r) * u1)) - (v - u) by RLVECT_1:41
.= ((- r) * (o - u1)) - (v - u) by RLVECT_1:48
.= (r * (- (o - u1))) - (v - u) by RLVECT_1:38
.= (o - u) - (v - u) by A1, RLVECT_1:47
.= o - ((v - u) + u) by RLVECT_1:41
.= o - v by RLSUB_2:78
.= 1 * (o - v) by RLVECT_1:def 9 ;
hence 1 * (o - v) = (- r) * (o - (u1 + (((- r) " ) * (v - u)))) ; :: thesis: verum

end;

A7: u1 + (((- r) " ) * (v - u)) = o + (((- r) " ) * (v - o))

proof

A8: (- r) * ((u1 + (((- r) " ) * (v - u))) - o) = r * (- ((u1 + (((- r) " ) * (v - u))) - o)) by RLVECT_1:38
.= r * (o - (u1 + (((- r) " ) * (v - u)))) by RLVECT_1:47
.= - (- (r * (o - (u1 + (((- r) " ) * (v - u)))))) by RLVECT_1:30
.= - (r * (- (o - (u1 + (((- r) " ) * (v - u)))))) by RLVECT_1:39
.= - (1 * (o - v)) by A6, RLVECT_1:38
.= - (o - v) by RLVECT_1:def 9
.= v - o by RLVECT_1:47 ;
thus u1 + (((- r) " ) * (v - u)) = o + ((u1 + (((- r) " ) * (v - u))) - o) by RLSUB_2:78
.= o + (((- r) " ) * (v - o)) by A4, A8, ANALOAF:13 ; :: thesis: verum

end;

A9: o,v '||' o,u1 + (((- r) " ) * (v - u))

proof

( v,o // u1 + (((- r) " ) * (v - u)),o or v,o // o,u1 + (((- r) " ) * (v - u)) ) by A6, ANALMETR:18;
then ( o,v // u1 + (((- r) " ) * (v - u)),o or o,v // o,u1 + (((- r) " ) * (v - u)) ) by ANALOAF:21;
hence o,v '||' o,u1 + (((- r) " ) * (v - u)) by GEOMTRAP:def 1; :: thesis: verum

end;

for r1, r2 being Real st (r1 * (u - o)) + (r2 * (v - o)) = 0. V holds
( r1 = 0 & r2 = 0 )

proof

let r1, r2 be Real; :: thesis: ( (r1 * (u - o)) + (r2 * (v - o)) = 0. V implies ( r1 = 0 & r2 = 0 ) )
assume A10: (r1 * (u - o)) + (r2 * (v - o)) = 0. V ; :: thesis: ( r1 = 0 & r2 = 0 )
assume ( r1 <> 0 or r2 <> 0 ) ; :: thesis: contradiction
then A11: ( r1 <> 0 or - r2 <> 0 ) ;
r1 * (u - o) = - (r2 * (v - o)) by A10, RLVECT_1:19
.= r2 * (- (v - o)) by RLVECT_1:39
.= (- r2) * (v - o) by RLVECT_1:38 ;
then ( o,u // o,v or o,u // v,o ) by A11, ANALMETR:18;
hence contradiction by A3, GEOMTRAP:def 1; :: thesis: verum

end;

then reconsider X = OASpace V as OAffinSpace by ANALOAF:38;
reconsider p = o, a = u, a1 = u1, b = v, b1 = v1, q = u1 + (((- r) " ) * (v - u)) as Element of X by Th4;
D12: o,v '||' o,v1 by A2;
E12: o,v '||' o,u1 + (((- r) " ) * (v - u)) by A9;
B12: u,v '||' u1,v1 by X;
C12: u,v '||' u1,u1 + (((- r) " ) * (v - u)) by B10;
o,u '||' o,u1 by B7;
then A12: ( p,a '||' p,a1 & a,b '||' a1,b1 & a,b '||' a1,q & p,b '||' p,b1 & p,b '||' p,q ) by E12, B12, C12, D12, Th5;
A13: not LIN p,b,a

proof

assume LIN p,b,a ; :: thesis: contradiction
then p,b '||' p,a by DIRAF:def 5;
then p,a '||' p,b by DIRAF:27;
hence contradiction by A3, Th5; :: thesis: verum

end;

( LIN p,b,b1 & LIN p,b,q & LIN p,a,a1 & b,a '||' a1,q & b,a '||' a1,b1 ) by A12, DIRAF:27, DIRAF:def 5;
hence ( v1 = u1 + (((- r) " ) * (v - u)) & v1 = o + (((- r) " ) * (v - o)) & v - u = (- r) * (v1 - u1) ) by A5, A7, A13, PASCH:11; :: thesis: verum