let I be Program of SCM+FSA; :: thesis: not halt SCM+FSA in rng (loop I)
thus not halt SCM+FSA in rng (loop I) by FUNCT_4:106; :: thesis: verum