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