let I, J be Program of {INT,(INT *)}; UsedIntLoc (I ';' J) = (UsedIntLoc I) \/ (UsedIntLoc J)
A1:
ProgramPart J = J
by RELAT_1:209;
dom I = dom (Directed I)
by FUNCT_4:105;
then
dom (Directed I) misses dom (Reloc ((ProgramPart J),(card I)))
by COMPOS_1:173;
hence UsedIntLoc (I ';' J) =
(UsedIntLoc (Directed I)) \/ (UsedIntLoc (Reloc ((ProgramPart J),(card I))))
by Th25, A1
.=
(UsedIntLoc I) \/ (UsedIntLoc (Reloc ((ProgramPart J),(card I))))
by Th30
.=
(UsedIntLoc I) \/ (UsedIntLoc J)
by Th29
;
verum