theorem :: PRE_CIRC:22

for f, g being finite Function st dom f misses dom g holds
card (f +* g) = (card f) + (card g)