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