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