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 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