theorem Th2: :: SCMPDS_7:2

for i, j, k being Instruction of SCMPDS
for I being Program of holds ((i ';' I) ';' j) ';' k = i ';' ((I ';' j) ';' k)