let I be Program of SCM+FSA; :: thesis: ( ( for s being State of SCM+FSA holds Initialized I is_halting_on s ) implies Initialized I is halting )
assume A1: for s being State of SCM+FSA holds Initialized I is_halting_on s ; :: thesis: Initialized I is halting

now

let s be State of SCM+FSA; :: thesis: ( Initialized I c= s implies ProgramPart s halts_on s )
Start-At (0,SCM+FSA) c= Initialized I by FUNCT_4:26;
then A2: s +* ((Initialized I) +* (Start-At (0,SCM+FSA))) = s +* (Initialized I) by FUNCT_4:79;
Initialized I is_halting_on s by A1;
then A3: ProgramPart (s +* ((Initialized I) +* (Start-At (0,SCM+FSA)))) halts_on s +* ((Initialized I) +* (Start-At (0,SCM+FSA))) by SCMFSA7B:def 8;
assume Initialized I c= s ; :: thesis: ProgramPart s halts_on s
then s +* ((Initialized I) +* (Start-At (0,SCM+FSA))) = s by A2, FUNCT_4:79;
hence ProgramPart s halts_on s by A3; :: thesis: verum

end;

hence Initialized I is halting by EXTPRO_1:def 10; :: thesis: verum