theorem Th41: :: SF_MASTR:41

for I being Program of
for k being Nat holds UsedI*Loc I = UsedI*Loc (Reloc (I,k))