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