let I, J be Program of SCM+FSA; :: 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 by CARD_1:104;
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:105 ;
A4: ProgramPart J = J by RELAT_1:209;
card (dom (Reloc (J,(card I)))) = card (Reloc (J,(card I))) by CARD_1:104
.= card J by COMPOS_1:174, A4
.= card (dom J) by CARD_1:104 ;
hence card (I ';' J) = (card I) + (card J) by A1, A2, A3, COMPOS_1:173, CARD_2:53, A4; :: thesis: verum