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 COMPOS_1:def 3;
hence Directed (I,l) = I by FUNCT_4:103; :: thesis: verum