let s be 0 -started State of SCM+FSA; :: according to AMISTD_1:def 11 :: thesis: for b₁ being set holds
( not f := p c= b₁ or b₁ halts_on s )
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( not f := p c= P or P halts_on s )
assume A3: f := p c= P ; :: thesis: P halts_on s
thus P halts_on s by Lm5, A3; :: thesis: verum