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 AFINSQ_1:def 3
.= i by Th10 ;
:: thesis: verum