let I, J be Program of SCMPDS ; :: thesis: card (I ';' J) = (card I) + (card J)
A1: ( card (dom (I ';' J)) = card (I ';' J) & card (dom I) = card I ) by CARD_1:104;
A2: ( card (dom J) = card J & dom (I ';' J) = (dom I) \/ (dom (Shift J,(card I))) ) by CARD_1:104, FUNCT_4:def 1;
card (dom (Shift J,(card I))) = card (Shift J,(card I)) by CARD_1:104
.= card J by Th3
.= card (dom J) by CARD_1:104 ;
hence card (I ';' J) = (card I) + (card J) by A1, A2, Th2, CARD_2:53; :: thesis: verum