let I, J be Program of ; :: thesis: UsedI*Loc (I ";" J) = (UsedI*Loc I) \/ (UsedI*Loc 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 UsedI*Loc (I ";" J) = UsedI*Loc ((stop (Directed I)) ';' J)
.= (UsedI*Loc (Directed I)) \/ (UsedI*Loc (Reloc (J,(card I)))) by A2, Th37, A1
.= (UsedI*Loc I) \/ (UsedI*Loc (Reloc (J,(card I)))) by Th42
.= (UsedI*Loc I) \/ (UsedI*Loc J) by Th41 ; :: thesis: verum