let I, J be Program of SCM+FSA ; :: thesis: (Directed I) ';' J = I ';' J
thus (Directed I) ';' J = (Directed I) +* (ProgramPart (Relocated J,(card (Directed I)))) by SCMFSA6A:63
.= I ';' J by Th33 ; :: thesis: verum