a := k = Load ((aSeq a,k) ^ <*(halt SCM+FSA )*>) by SCMFSA_7:33;
hence ( a := k is initial & a := k is NAT -defined & a := k is the Instructions of SCM+FSA -valued ) ; :: thesis: verum