let n be non zero Nat; :: thesis: for X being non-empty n -element FinSequence
for S being SemialgebraFamily of X
for i being Nat st i in Seg n holds
X . i in S . i
let X be non-empty n -element FinSequence; :: thesis: for S being SemialgebraFamily of X
for i being Nat st i in Seg n holds
X . i in S . i
let S be SemialgebraFamily of X; :: thesis: for i being Nat st i in Seg n holds
X . i in S . i

hereby :: thesis: verum

let i be Nat; :: thesis: ( i in Seg n implies X . i in S . i )
assume i in Seg n ; :: thesis: X . i in S . i
then S . i is semialgebra_of_sets of X . i by Def2;
hence X . i in S . i by SRINGS_3:def 6; :: thesis: verum

end;