theorem Th2: :: SCMPDS_6:7

for i being Instruction of SCMPDS
for I being Program of holds (i ';' I) . 0 = i