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