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

now

let s be State of SCM+FSA ; :: thesis: ( Initialized I c= s implies s is halting )
assume A2: Initialized I c= s ; :: thesis: s is halting
I is_halting_on Initialize s by A1;
then (Initialize s) +* (I +* (Start-At (insloc 0 ))) is halting by SCMFSA7B:def 8;
then s +* (Initialized I) is halting by SCMFSA8A:13;
hence s is halting by A2, FUNCT_4:79; :: thesis: verum

end;

hence Initialized I is halting by AMI_1:def 26; :: thesis: verum