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