theorem Th9: :: COMPOS_1:18

for S being COM-Struct
for F being Program of S
for G being non empty preProgram of S holds dom (CutLastLoc F) misses dom (Reloc (G,((card F) -' 1)))