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 destroys intloc 0 by SCMFSA7B:def 5;
then not ProgramPart (Relocated (I,n)) destroys intloc 0 by Th23;
hence ProgramPart (Relocated (I,n)) is good by SCMFSA7B:def 5; :: thesis: verum