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