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