f := p = Load ((((aSeq (intloc 1),(len p)) ^ <*(f :=<0,...,0> (intloc 1))*>) ^ (aSeq f,p)) ^ <*(halt SCM+FSA )*>) by SCMFSA_7:def 5;
hence ( f := p is initial & f := p is NAT -defined ) ; :: thesis: verum