let I, J be Program of SCM+FSA ; :: thesis: UsedIntLoc (I ';' J) = (UsedIntLoc I) \/ (UsedIntLoc 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 UsedIntLoc (I ';' J) = (UsedIntLoc (Directed I)) \/ (UsedIntLoc (ProgramPart (Relocated J,(card I)))) by Th25
.= (UsedIntLoc I) \/ (UsedIntLoc (ProgramPart (Relocated J,(card I)))) by Th30
.= (UsedIntLoc I) \/ (UsedIntLoc J) by Th29 ;
:: thesis: verum