let I, J be Program of {INT,(INT *)}; UsedInt*Loc (I ';' J) = (UsedInt*Loc I) \/ (UsedInt*Loc 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 UsedInt*Loc (I ';' J) =
(UsedInt*Loc (Directed I)) \/ (UsedInt*Loc (Reloc ((ProgramPart J),(card I))))
by Th41, A1
.=
(UsedInt*Loc I) \/ (UsedInt*Loc (Reloc ((ProgramPart J),(card I))))
by Th46
.=
(UsedInt*Loc I) \/ (UsedInt*Loc J)
by Th45
;
verum