theorem Th68: :: CARD_3:68

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