<*x1,x2,x3,x4*> = <*x1,x2,x3*> ^ <*x4*> ;
hence <*x1,x2,x3,x4*> is FinSequence of D ; :: thesis: verum