let I be Program of SCM+FSA; :: thesis: ( ( for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_on Initialized s,P ) implies Initialized I is halting )
A1: ProgramPart I = I by RELAT_1:209;
A2: ProgramPart (Initialized I) = I by SCMFSA6A:33;
assume A3: for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_on Initialized s,P ; :: thesis: Initialized I is halting

now

let s be State of SCM+FSA; :: thesis: ( Initialized I c= s implies for P1 being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P1 holds
P1 halts_on s )
assume Initialized I c= s ; :: thesis: for P1 being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P1 holds
P1 halts_on s
then A4: s +* (Initialized I) = s by FUNCT_4:79;
let P1 be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( I c= P1 implies P1 halts_on s )
assume A5: I c= P1 ; :: thesis: P1 halts_on s
A6: P1 +* I = P1 by A5, FUNCT_4:79;
I is_halting_on Initialized s,P1 by A3;
then A7: P1 +* I halts_on (Initialized s) +* (Initialize I) by SCMFSA7B:def 8, A1;
(Initialized s) +* (Initialize I) = s +* (Initialized I) by SCMFSA8A:13;
then P1 +* I halts_on s +* (Initialized I) by A7;
hence P1 halts_on s by A4, A6; :: thesis: verum

end;

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