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