theorem Th4: :: SCMFSA8A:11

for I, J being preProgram of SCM+FSA
for a being Int-Location st not I destroys a & not J destroys a holds
not I +* J destroys a