let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA holds
( Initialized I is_halting_on s iff I is_halting_on Initialized s )
let I be Program of SCM+FSA ; :: thesis: ( Initialized I is_halting_on s iff I is_halting_on Initialized s )
X: s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )) by Th16;

hereby :: thesis: ( I is_halting_on Initialized s implies Initialized I is_halting_on s )

assume Initialized I is_halting_on s ; :: thesis: I is_halting_on Initialized s
then ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) by SCMFSA7B:def 8;
then ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) halts_on (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )) by X;
hence I is_halting_on Initialized s by SCMFSA7B:def 8; :: thesis: verum

end;

assume I is_halting_on Initialized s ; :: thesis: Initialized I is_halting_on s
then ProgramPart ((Initialized s) +* (I +* (Start-At 0 ,SCM+FSA ))) halts_on (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )) by SCMFSA7B:def 8;
then ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) by X;
hence Initialized I is_halting_on s by SCMFSA7B:def 8; :: thesis: verum