for V being RealLinearSpace
for u, v, w being VECTOR of V holds u,v '||' w # u,w # v by Th8;