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