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