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

proof

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

end;

hence S is SemialgebraFamily of X by Def2; :: thesis: verum