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