let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V holds u,v // u,v
let u, v be VECTOR of V; :: thesis: u,v // u,v
( 1 * (v - u) = 1 * (v - u) & 0 < 1 ) ;
hence u,v // u,v by Def1; :: thesis: verum