let I, J be Program of ; card (I ';' J) = (card I) + (card J)
A1:
( card (dom (I ';' J)) = card (I ';' J) & card (dom I) = card I )
by CARD_1:62;
A2:
card (dom J) = card J
by CARD_1:62;
A3: dom (I ';' J) =
(dom (Directed I)) \/ (dom (Reloc (J,(card I))))
by FUNCT_4:def 1
.=
(dom I) \/ (dom (Reloc (J,(card I))))
by FUNCT_4:99
;
card (dom (Reloc (J,(card I)))) =
card (Reloc (J,(card I)))
by CARD_1:62
.=
card J
by COMPOS_1:49
.=
card (dom J)
by CARD_1:62
;
hence
card (I ';' J) = (card I) + (card J)
by A1, A2, A3, CARD_2:40, COMPOS_1:48; verum