let I be preProgram of SCM+FSA ; :: thesis: for l being Element of NAT st I is halt-free holds
Directed I,l = I
let l be Element of NAT ; :: thesis: ( I is halt-free implies Directed I,l = I )
assume I is halt-free ; :: thesis: Directed I,l = I
then not halt SCM+FSA in rng I by AMI_1:def 53;
hence Directed I,l = I by FUNCT_4:109; :: thesis: verum