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