theorem Th70: :: CARD_3:70

for f, g, h being Function st g in sproduct f & h in sproduct f holds
g +* h in sproduct f