not halt SCM+FSA in rng (Directed (P,l)) by FUNCT_4:106;
hence Directed (P,l) is halt-free by COMPOS_1:def 7; :: thesis: verum