theorem Th25: :: SF_MASTR:25

for I being Program of
for k being Nat holds UsedILoc I = UsedILoc (Reloc (I,k))