for f, g being Function st product f <> {} holds
( g in sproduct f iff ex h being Function st
( h in product f & g c= h ) )