let I, J be Program of SCM+FSA; :: thesis: Directed (I ';' J) = I ';' (Directed J)
thus I ';' (Directed J) = (Directed I) +* (Directed ((ProgramPart (Relocated (J,(card I)))),((card I) + (card J)))) by Th65
.= (Directed I) +* (Directed ((ProgramPart (Relocated (J,(card I)))),(card (I ';' J)))) by Th61
.= (Directed ((Directed I),(card (I ';' J)))) +* (Directed ((ProgramPart (Relocated (J,(card I)))),(card (I ';' J)))) by Th63
.= Directed (I ';' J) by FUNCT_7:119 ; :: thesis: verum