let I be preProgram of SCM+FSA ; :: thesis: for l being Instruction-Location of SCM+FSA st I is halt-free holds
Directed I,l = I
let l be Instruction-Location of SCM+FSA ; :: 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 52;
hence Directed I,l = I by FUNCT_4:109; :: thesis: verum