let I, J be Program of ; :: thesis: UsedInt*Loc (I ';' J) = (UsedInt*Loc I) \/ (UsedInt*Loc 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 UsedInt*Loc (I ';' J) = (UsedInt*Loc (Directed I)) \/ (UsedInt*Loc (Reloc (J,(card I)))) by Th41
.= (UsedInt*Loc I) \/ (UsedInt*Loc (Reloc (J,(card I)))) by Th46
.= (UsedInt*Loc I) \/ (UsedInt*Loc J) by Th45 ;
:: thesis: verum