theorem :: SCMPDS_4:10

for i, j being Instruction of SCMPDS holds i ';' j = i ';' (Load j) ;