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 Th21
.= card ((dom f) \/ (dom g)) by FUNCT_4:def 1
.= (card (dom f)) + (card (dom g)) by A1, CARD_2:53
.= (card (dom f)) + (card g) by Th21
.= (card f) + (card g) by Th21 ; :: thesis: verum