let I, J be Program of ; Directed (I ";" J) = I ";" (Directed J)
A1:
(card (stop I)) -' 1 = card I
by COMPOS_1:71;
A2:
card (stop (Directed I)) = card (stop I)
by Lm2;
hence I ";" (Directed J) =
(Directed I) +* ((Reloc (J,(card I))) +~ ((halt SCM+FSA),(goto ((card J) + (card I)))))
by Th13, A1
.=
(Directed I) +* ((Reloc (J,(card I))) +~ ((halt SCM+FSA),(goto (card (I ";" J)))))
by Th11
.=
((Directed I) +~ ((halt SCM+FSA),(goto (card (I ";" J))))) +* ((Reloc (J,(card I))) +~ ((halt SCM+FSA),(goto (card (I ";" J)))))
by FUNCT_4:127
.=
Directed (I ";" J)
by FUNCT_7:117, A1, A2
;
verum