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 Th6;
hence ((I ';' i) ';' J) . (card I) = (I ';' i) . (card I) by AFINSQ_1:def 3
.= i by Th6 ;
:: thesis: verum