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) and
A2: r <> 0 and
A3: o,v '||' o,v1 and
A4: not o,u '||' o,v and
A5: u,v '||' u1,v1 ; :: thesis: ( v1 = u1 + (((- r) " ) * (v - u)) & v1 = o + (((- r) " ) * (v - o)) & v - u = (- r) * (v1 - u1) )
A6: - r <> 0 by A2;
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 (r1 * (u - o)) + (r2 * (v - o)) = 0. V ; :: thesis: ( r1 = 0 & r2 = 0 )
then A7: r1 * (u - o) = - (r2 * (v - o)) by RLVECT_1:19
.= r2 * (- (v - o)) by RLVECT_1:39
.= (- r2) * (v - o) by RLVECT_1:38 ;
assume ( r1 <> 0 or r2 <> 0 ) ; :: thesis: contradiction
then ( r1 <> 0 or - r2 <> 0 ) ;
then ( o,u // o,v or o,u // v,o ) by A7, ANALMETR:18;
hence contradiction by A4, GEOMTRAP:def 1; :: thesis: verum

end;

then reconsider X = OASpace V as OAffinSpace by ANALOAF:38;
set w = u1 + (((- r) " ) * (v - u));
reconsider p = o, a = u, a1 = u1, b = v, b1 = v1, q = u1 + (((- r) " ) * (v - u)) as Element of X by Th4;
a,b '||' a1,b1 by A5, Th5;
then A8: b,a '||' a1,b1 by DIRAF:27;
p,b '||' p,b1 by A3, Th5;
then A9: LIN p,b,b1 by DIRAF:def 5;
A10: (- r) * ((u1 + (((- r) " ) * (v - u))) - u1) = (- r) * (((- r) " ) * (v - u)) by RLSUB_2:78
.= ((- r) * ((- r) " )) * (v - u) by RLVECT_1:def 10
.= 1 * (v - u) by A6, XCMPLX_0:def 7 ;
then A11: v - u = (- r) * ((u1 + (((- r) " ) * (v - u))) - u1) by RLVECT_1:def 11;
( u,v // u1,u1 + (((- r) " ) * (v - u)) or u,v // u1 + (((- r) " ) * (v - u)),u1 ) by A10, ANALMETR:18;
then u,v '||' u1,u1 + (((- r) " ) * (v - u)) by GEOMTRAP:def 1;
then a,b '||' a1,q by Th5;
then A12: b,a '||' a1,q by DIRAF:27;
A13: (- 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 8
.= ((- r) * o) - (((- r) * u1) + (((- r) * ((- r) " )) * (v - u))) by RLVECT_1:def 10
.= ((- r) * o) - (((- r) * u1) + (1 * (v - u))) by A6, XCMPLX_0:def 7
.= ((- r) * o) - (((- r) * u1) + (v - u)) by RLVECT_1:def 11
.= (((- 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 11 ;
then ( v,o // u1 + (((- r) " ) * (v - u)),o or v,o // o,u1 + (((- r) " ) * (v - u)) ) by ANALMETR:18;
then ( o,v // u1 + (((- r) " ) * (v - u)),o or o,v // o,u1 + (((- r) " ) * (v - u)) ) by ANALOAF:21;
then o,v '||' o,u1 + (((- r) " ) * (v - u)) by GEOMTRAP:def 1;
then p,b '||' p,q by Th5;
then A14: LIN p,b,q by DIRAF:def 5;
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 10
.= (- r) * (u1 - o) ;
then ( o,u // o,u1 or o,u // u1,o ) by ANALMETR:18;
then o,u '||' o,u1 by GEOMTRAP:def 1;
then p,a '||' p,a1 by Th5;
then A15: LIN p,a,a1 by DIRAF:def 5;
A16: 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 A4, Th5; :: thesis: verum

end;

A17: (- 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 A13, RLVECT_1:38
.= - (o - v) by RLVECT_1:def 11
.= v - o by RLVECT_1:47 ;
u1 + (((- r) " ) * (v - u)) = o + ((u1 + (((- r) " ) * (v - u))) - o) by RLSUB_2:78
.= o + (((- r) " ) * (v - o)) by A6, A17, ANALOAF:13 ;
hence ( v1 = u1 + (((- r) " ) * (v - u)) & v1 = o + (((- r) " ) * (v - o)) & v - u = (- r) * (v1 - u1) ) by A11, A16, A9, A14, A15, A12, A8, PASCH:11; :: thesis: verum