let V be RealLinearSpace; :: thesis: for u, v being VECTOR of V holds u,u # v // u # v,v
let u, v be VECTOR of V; :: thesis: u,u # v // u # v,v
set p = u # v;
2 * ((u # v) - u) = v - u by Th10
.= 2 * (v - (u # v)) by Th10 ;
hence u,u # v // u # v,v by ANALOAF:def 1; :: thesis: verum