let i be Instruction of SCMPDS; :: thesis: for I being Program of SCMPDS holds card (I ';' i) = (card I) + 1
let I be Program of SCMPDS; :: thesis: card (I ';' i) = (card I) + 1
thus card (I ';' i) = card (I ';' (Load i)) by SCMPDS_4:def 3
.= (card I) + (card (Load i)) by AFINSQ_1:17
.= (card I) + 1 by COMPOS_1:54 ; :: thesis: verum