let f, g be finite Function; :: thesis: ( dom f misses dom g implies card (f +* g) = (card f) + (card g) )
assume A1: dom f misses dom g ; :: thesis: card (f +* g) = (card f) + (card g)
thus card (f +* g) = card (dom (f +* g)) by CARD_1:62
.= card ((dom f) \/ (dom g)) by FUNCT_4:def 1
.= (card (dom f)) + (card (dom g)) by A1, CARD_2:40
.= (card (dom f)) + (card g) by CARD_1:62
.= (card f) + (card g) by CARD_1:62 ; :: thesis: verum