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 5
.= (card I) + (card (Load i)) by SCMPDS_4:45
.= (card I) + 1 by SCMPDS_5:6 ; :: thesis: verum