theorem :: CARD_3:69

for f, g, f9, g9 being Function st dom f9 misses (dom g) \ (dom g9) & f9 in sproduct f & g9 in sproduct g holds
f9 +* g9 in sproduct (f +* g)