<*v,u,w*> = <*v,u*> ^ <*w*> by FINSEQ_1:60;
hence <*v,u,w*> is FinSequence of V ; :: thesis: verum