theorem Th3: :: SCMPDS_5:14

for I, J being Program of holds (stop I) +* (stop (I ';' J)) = stop (I ';' J)