:: deftheorem Def2 defines SemiringFamily SRINGS_4:def 3 :
for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for b₃ being b₁ -element FinSequence holds
( b₃ is SemiringFamily of X iff for i being Nat st i in Seg n holds
b₃ . i is semiring_of_sets of (X . i) );