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