A1: IC in dom (Initialize (f := p)) by COMPOS_1:141;
let s be State of SCM+FSA; :: according to SCMFSA6B:def 3,EXTPRO_1:def 10 :: thesis: ( not Initialize (f := p) c= s or for b₁ being set holds
( not ProgramPart (Initialize (f := p)) c= b₁ or b₁ halts_on s ) )
assume A2: Initialize (f := p) c= s ; :: thesis: for b₁ being set holds
( not ProgramPart (Initialize (f := p)) c= b₁ or b₁ halts_on s )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( not ProgramPart (Initialize (f := p)) c= P or P halts_on s )
assume A3: ProgramPart (Initialize (f := p)) c= P ; :: thesis: P halts_on s
A4: f := p c= P by A3, COMPOS_1:144;
IC s = IC (Initialize (f := p)) by A2, A1, GRFUNC_1:8
.= 0 by COMPOS_1:142 ;
then s is 0 -started by COMPOS_1:def 20;
hence P halts_on s by Lm5, A4; :: thesis: verum