<*a1,a2,a3,a4,a5*> ^ <*a6*> is FinSequence of X ;
hence <*a1,a2,a3,a4,a5,a6*> is FinSequence of X ; :: thesis: verum