let I, J be good preProgram of SCM+FSA; :: thesis: I +* J is good
( not I destroys intloc 0 & not J destroys intloc 0 ) by SCMFSA7B:def 5;
then not I +* J destroys intloc 0 by Th4;
hence I +* J is good by SCMFSA7B:def 5; :: thesis: verum