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

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