:: deftheorem Def3 defines SemiringProduct SRINGS_4:def 4 :
for n being non zero Nat
for X being b₁ -element FinSequence
for b₃ being set holds
( b₃ = SemiringProduct X iff for f being object holds
( f in b₃ iff ex g being Function st
( f = product g & g in product X ) ) );