A: halt SCM+FSA in rng I by COMPOS_1:def 7;
I c= Initialized I by Th26;
then rng I c= rng (Initialized I) by RELAT_1:25;
hence halt SCM+FSA in rng (Initialized I) by A; :: according to COMPOS_1:def 7 :: thesis: verum