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