let V be RealLinearSpace; :: thesis: for u, v, w being VECTOR of V holds u,v '||' w # u,w # v
let u, v, w be VECTOR of V; :: thesis: u,v '||' w # u,w # v
u,v // w # u,w # v by Th10;
hence u,v '||' w # u,w # v by Def1; :: thesis: verum