for f, g, h being Function st h in sproduct (f +* g) holds
ex f9, g9 being Function st
( f9 in sproduct f & g9 in sproduct g & h = f9 +* g9 )