let i be Instruction of SCMPDS ; :: thesis: for I, J being Program of SCMPDS holds ((I ';' i) ';' J) . (inspos (card I)) = i
let I, J be Program of SCMPDS ; :: thesis: ((I ';' i) ';' J) . (inspos (card I)) = i
inspos (card I) in dom (I ';' i) by Th10;
hence ((I ';' i) ';' J) . (inspos (card I)) = (I ';' i) . (inspos (card I)) by SCMPDS_4:37
.= i by Th10 ;
:: thesis: verum