let V be RealLinearSpace; for u, v being VECTOR of V st u,v // v,u holds
u = v
let u, v be VECTOR of V; ( u,v // v,u implies u = v )
assume A1:
u,v // v,u
; u = v
assume A2:
u <> v
; contradiction
then consider a, b being Real such that
A3:
a * (v - u) = b * (u - v)
and
A4:
( 0 < a & 0 < b )
by A1;
a * (v - u) = - (b * (v - u))
by A3, Th3;
then
(b * (v - u)) + (a * (v - u)) = 0. V
by RLVECT_1:5;
then
(b + a) * (v - u) = 0. V
by RLVECT_1:def 6;
then
( v - u = 0. V or b + a = 0 )
by RLVECT_1:11;
then
0. V = (- u) + v
by A4;
then v =
- (- u)
by RLVECT_1:def 10
.=
u
by RLVECT_1:17
;
hence
contradiction
by A2; verum