let I be good preProgram of SCM+FSA; :: thesis: for n being Element of NAT holds Reloc (I,n) is good
let n be Element of NAT ; :: thesis: Reloc (I,n) is good
not I destroys intloc 0 by SCMFSA7B:def 5;
then not Reloc (I,n) destroys intloc 0 by Th2;
hence Reloc (I,n) is good by SCMFSA7B:def 5; :: thesis: verum