let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V st u,v // v,u holds

u = v

let u, v be VECTOR of V; :: thesis: ( u,v // v,u implies u = v )

assume A1: u,v // v,u ; :: thesis: u = v

assume A2: u <> v ; :: thesis: 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; :: thesis: verum

u = v

let u, v be VECTOR of V; :: thesis: ( u,v // v,u implies u = v )

assume A1: u,v // v,u ; :: thesis: u = v

assume A2: u <> v ; :: thesis: 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; :: thesis: verum