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