let I, J be Program of ; :: thesis: UsedIntLoc (I ';' J) = (UsedIntLoc I) \/ (UsedIntLoc J)
dom I = dom (Directed I) by FUNCT_4:99;
then dom (Directed I) misses dom (Reloc (J,(card I))) by COMPOS_1:48;
hence UsedIntLoc (I ';' J) = (UsedIntLoc (Directed I)) \/ (UsedIntLoc (Reloc (J,(card I)))) by Th25
.= (UsedIntLoc I) \/ (UsedIntLoc (Reloc (J,(card I)))) by Th30
.= (UsedIntLoc I) \/ (UsedIntLoc J) by Th29 ;
:: thesis: verum