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