theorem :: SCMFSA8A:25

for I, J being Program of SCM+FSA holds (Directed I) ";" J = I ";" J ;