let s be State of SCM+FSA; :: according to EXTPRO_1:def 10 :: thesis: ( not Initialized I c= s or for b₁ being set holds
( not ProgramPart (Initialized I) c= b₁ or b₁ halts_on s ) )
assume A1: Initialized I c= s ; :: thesis: for b₁ being set holds
( not ProgramPart (Initialized I) c= b₁ or b₁ halts_on s )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not ProgramPart (Initialized I) c= P or P halts_on s )
assume A2: ProgramPart (Initialized I) c= P ; :: thesis: P halts_on s
ProgramPart (Initialized I) = I by SCMFSA6A:33;
hence P halts_on s by A1, A2, Th19; :: thesis: verum