let I, J be Program of SCM+FSA ; :: thesis: UsedInt*Loc (I ';' J) = (UsedInt*Loc I) \/ (UsedInt*Loc J)
dom I = dom (Directed I) by FUNCT_4:105;
then A1: dom (Directed I) misses dom (ProgramPart (Relocated J,(card I))) by SCMFSA6A:16;
thus UsedInt*Loc (I ';' J) = (UsedInt*Loc (Directed I)) \/ (UsedInt*Loc [(ProgramPart (Relocated J,(card I)))]) by A1, Th41
.= (UsedInt*Loc I) \/ (UsedInt*Loc (ProgramPart (Relocated J,(card I)))) by Th46
.= (UsedInt*Loc I) \/ (UsedInt*Loc J) by Th45 ; :: thesis: verum