let I, J be Program of ; UsedIntLoc (I ';' J) = (UsedIntLoc I) \/ (UsedIntLoc J)
dom I = dom (Directed I)
by FUNCT_4:105;
then
dom (Directed I) misses dom (ProgramPart (Relocated J,(card I)))
by SCMFSA6A:16;
hence UsedIntLoc (I ';' J) =
(UsedIntLoc (Directed I)) \/ (UsedIntLoc [(ProgramPart (Relocated J,(card I)))])
by Th25
.=
(UsedIntLoc I) \/ (UsedIntLoc [(ProgramPart (Relocated J,(card I)))])
by Th30
.=
(UsedIntLoc I) \/ (UsedIntLoc J)
by Th29
;
verum