let s be State of SCM+FSA; :: according to EXTPRO_1:def 10 :: thesis: ( not Initialized I c= s or ProgramPart s halts_on s )
assume Initialized I c= s ; :: thesis: ProgramPart s halts_on s
hence ProgramPart s halts_on s by Th19; :: thesis: verum