let n be non zero Nat; :: thesis: for X being non-empty n -element FinSequence
for S being FieldFamily of X holds S is SemialgebraFamily of X
let X be non-empty n -element FinSequence; :: thesis: for S being FieldFamily of X holds S is SemialgebraFamily of X
let S be FieldFamily of X; :: thesis: S is SemialgebraFamily of X
for i being Nat st i in Seg n holds
S . i is semialgebra_of_sets of X . i by SRINGS_3:20;
hence S is SemialgebraFamily of X by Def2; :: thesis: verum