let i, j be Instruction of SCMPDS ; :: thesis: for I being Program of SCMPDS holds card ((i ';' j) ';' I) = (card I) + 2
let I be Program of SCMPDS ; :: thesis: card ((i ';' j) ';' I) = (card I) + 2
thus card ((i ';' j) ';' I) = card (i ';' (j ';' I)) by SCMPDS_4:52
.= (card (j ';' I)) + 1 by Th15
.= ((card I) + 1) + 1 by Th15
.= (card I) + 2 ; :: thesis: verum