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 A1: dom (Directed I) misses dom (ProgramPart (Relocated J,(card I))) by SCMFSA6A:16;
thus UsedIntLoc (I ';' J) = (UsedIntLoc (Directed I)) \/ (UsedIntLoc [(ProgramPart (Relocated J,(card I)))]) by A1, Th25
.= (UsedIntLoc I) \/ (UsedIntLoc [(ProgramPart (Relocated J,(card I)))]) by Th30
.= (UsedIntLoc I) \/ (UsedIntLoc J) by Th29 ; :: thesis: verum