a
:=
k
=
(
aSeq
(
a
,
k
)
)
^
(
Stop
SCM+FSA
)
by
SCMFSA_7:1
;
hence
(
a
:=
k
is
initial
& not
a
:=
k
is
empty
&
a
:=
k
is
NAT
-defined
&
a
:=
k
is the
InstructionsF
of
SCM+FSA
-valued
) ;
:: thesis:
verum