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