theorem Th5: :: SCMFSA8A:12

for I, J being good preProgram of SCM+FSA holds I +* J is good