let i, j be Instruction of SCMPDS; :: thesis: card (i ';' j) = 2
thus card (i ';' j) = card ((Load i) ';' (Load j)) by SCMPDS_4:def 4
.= (card (Load i)) + (card (Load j)) by AFINSQ_1:17
.= 1 + (card (Load j)) by COMPOS_1:54
.= 1 + 1 by COMPOS_1:54
.= 2 ; :: thesis: verum