theorem Thm19: :: SRINGS_4:21

for n being non zero Nat
for X being b₁ -element FinSequence holds SemiringProduct X c= bool (Funcs ((dom X),(union (Union X))))