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