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