for f, g, h being Function st g tolerates h & g in sproduct f & h in sproduct f holds
g \/ h in sproduct f