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