let I, J be Program of ; :: thesis: UsedILoc (I ";" J) = (UsedILoc I) \/ (UsedILoc J)
A1: (card (stop (Directed I))) -' 1 = card (Directed I) by COMPOS_1:71
.= card I by SCMFSA6A:36 ;
dom I = dom (Directed I) by FUNCT_4:99;
then A2: dom (Directed I) misses dom (Reloc (J,(card I))) by COMPOS_1:48;
thus UsedILoc (I ";" J) = UsedILoc ((stop (Directed I)) ';' J)
.= (UsedILoc (Directed I)) \/ (UsedILoc (Reloc (J,(card I)))) by A2, Th21, A1
.= (UsedILoc I) \/ (UsedILoc (Reloc (J,(card I)))) by Th26
.= (UsedILoc I) \/ (UsedILoc J) by Th25 ; :: thesis: verum