let I, J be Program of ; :: thesis: card (I ";" J) = (card I) + (card J)
A1: ( card (dom (I ";" J)) = card (I ";" J) & card (dom I) = card I ) ;
A2: card (stop (Directed I)) = card (stop I) by Lm2;
(card (stop I)) -' 1 = card I by COMPOS_1:71;
then A3: dom (I ";" J) = (dom (Directed I)) \/ (dom (Reloc (J,(card I)))) by FUNCT_4:def 1, A2
.= (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) ;
hence card (I ";" J) = (card I) + (card J) by A1, A3, CARD_2:40, COMPOS_1:48; :: thesis: verum