let I, J be Program of ; Directed (I ";" J) = I ";" (Directed J)
thus I ";" (Directed J) =
(Directed I) +* (Directed ((Reloc (J,(card I))),((card I) + (card J))))
by Th65
.=
(Directed I) +* (Directed ((Reloc (J,(card I))),(card (I ";" J))))
by Th61
.=
(Directed ((Directed I),(card (I ";" J)))) +* (Directed ((Reloc (J,(card I))),(card (I ";" J))))
by Th63
.=
Directed (I ";" J)
by FUNCT_7:117
; verum