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