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