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 by CARD_1:47 ;

now

assume halt SCM+FSA in rng (Load (<*> the Instructions of SCM+FSA )) ; :: thesis: contradiction
then consider x being set such that
A2: 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;
dom (Load (<*> the Instructions of SCM+FSA )) c= NAT by RELAT_1:def 18;
then reconsider x = x as Instruction-Location of SCM+FSA by A2, AMI_1:def 4;
reconsider k = x as Element of NAT by ORDINAL1:def 13;
x = insloc k ;
hence contradiction by A1, A2, SCMFSA6A:15; :: thesis: verum

end;

then A4: Load (<*> the Instructions of SCM+FSA ) is halt-free by AMI_1:def 52;

now

let i be Instruction of SCM+FSA ; :: thesis: ( i in rng (Load (<*> the Instructions of SCM+FSA )) implies i does_not_destroy intloc 0 )
assume ( i in rng (Load (<*> the Instructions of SCM+FSA )) & not i does_not_destroy intloc 0 ) ; :: 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 = i by FUNCT_1:def 5;
dom (Load (<*> the Instructions of SCM+FSA )) c= NAT by RELAT_1:def 18;
then reconsider x = x as Instruction-Location of SCM+FSA by A5, AMI_1:def 4;
reconsider k = x as Element of NAT by ORDINAL1:def 13;
A6: x = insloc k ;
thus contradiction by A1, A5, A6, SCMFSA6A:15; :: thesis: verum

end;

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