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)))],(insloc ((card I) + (card J)))) by Th50
.= (Directed I) +* (Directed [(ProgramPart (Relocated J,(card I)))],(insloc (card (I ';' J)))) by Th61
.= (Directed (Directed I),(insloc (card (I ';' J)))) +* (Directed [(ProgramPart (Relocated J,(card I)))],(insloc (card (I ';' J)))) by Th39
.= Directed (I ';' J) by FUNCT_7:119 ; :: thesis: verum