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