let s be State of SCM+FSA; :: thesis: for I being InitHalting Program of SCM+FSA st Initialized I c= s holds
ProgramPart s halts_on s
let I be InitHalting Program of SCM+FSA; :: thesis: ( Initialized I c= s implies ProgramPart s halts_on s )
assume A1: Initialized I c= s ; :: thesis: ProgramPart s halts_on s
Initialized I is halting by Def2;
hence ProgramPart s halts_on s by A1, EXTPRO_1:def 10; :: thesis: verum