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) & 0 < a & 0 < b ) by A1, Th16;
a * (v - u) = - (b * (v - u)) by A3, Th10;
then (b * (v - u)) + (a * (v - u)) = 0. V by RLVECT_1:16;
then (b + a) * (v - u) = 0. V by RLVECT_1:def 9;
then ( v - u = 0. V or b + a = 0 ) by RLVECT_1:24;
then 0. V = (- u) + v by A3, XREAL_1:36;
then v = - (- u) by RLVECT_1:def 11
.= u by RLVECT_1:30 ;
hence contradiction by A2; :: thesis: verum