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 i does_not_destroy intloc 0 )
assume that
A2: i in rng (Load (<*> the Instructions of SCM+FSA )) and
not i does_not_destroy 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;
dom (Load (<*> the Instructions of SCM+FSA )) c= NAT by RELAT_1:def 18;
then reconsider x = x as Element of NAT by A3;
reconsider k = x as Element of NAT ;
x = k ;
hence contradiction by A1, A3, SCMFSA6A:15; :: thesis: verum

end;

then Load (<*> the Instructions of SCM+FSA ) does_not_destroy 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;
dom (Load (<*> the Instructions of SCM+FSA )) c= NAT by RELAT_1:def 18;
then reconsider x = x as Element of NAT by A5;
reconsider k = x as Element of NAT ;
x = k ;
hence contradiction by A1, A5, SCMFSA6A:15; :: thesis: verum

end;

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