for n being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being SemialgebraFamily of X
for i being Nat st i in Seg n holds
X . i in S . i