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 Th21
.= (UsedIntLoc I) \/ (UsedIntLoc (Reloc (J,(card I)))) by Th26
.= (UsedIntLoc I) \/ (UsedIntLoc J) by Th25 ;
:: thesis: verum