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
jj * (v - u) = jj * (v - u) ;
hence u,v // u,v ; :: thesis: verum