theorem Th42: :: SF_MASTR:42

for I being Program of holds UsedI*Loc I = UsedI*Loc (Directed I)