theorem Th7: :: SCMFSA8A:14

for I, J being Program of SCM+FSA
for x being set st x in dom I holds
(I ";" J) . x = (Directed I) . x