set I = Load (<*> the Instructions of SCM+FSA );
A1: card (Load (<*> the Instructions of SCM+FSA )) = len (<*> the Instructions of SCM+FSA ) by SCMFSA_7:25
.= 0 ;

now

let i be Instruction of SCM+FSA ; :: thesis: ( i in rng (Load (<*> the Instructions of SCM+FSA )) implies not i destroysdestroy intloc 0 )
assume that
A2: i in rng (Load (<*> the Instructions of SCM+FSA )) and
i destroysdestroy intloc 0 ; :: thesis: contradiction
consider x being set such that
A3: x in dom (Load (<*> the Instructions of SCM+FSA )) and
(Load (<*> the Instructions of SCM+FSA )) . x = i by A2, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A3;
reconsider k = x as Element of NAT ;
thus contradiction by A1, A3; :: thesis: verum

end;

then not Load (<*> the Instructions of SCM+FSA ) destroysdestroy intloc 0 by Def4;
then A4: Load (<*> the Instructions of SCM+FSA ) is good by Def5;

now

assume halt SCM+FSA in rng (Load (<*> the Instructions of SCM+FSA )) ; :: thesis: contradiction
then consider x being set such that
A5: x in dom (Load (<*> the Instructions of SCM+FSA )) and
(Load (<*> the Instructions of SCM+FSA )) . x = halt SCM+FSA by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A5;
reconsider k = x as Element of NAT ;
thus contradiction by A1, A5; :: thesis: verum

end;

then Load (<*> the Instructions of SCM+FSA ) is halt-free by COMPOS_1:def 7;
hence ex b₁ being Program of SCM+FSA st
( b₁ is halt-free & b₁ is good ) by A4; :: thesis: verum