theorem Th43: :: SF_MASTR:43

for I, J being Program of holds UsedI*Loc (I ";" J) = (UsedI*Loc I) \/ (UsedI*Loc J)