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 Th19 ; :: thesis: verum