let n be non zero Nat; :: thesis: for X being non-empty n -element FinSequence
for S being SemialgebraFamily of X holds S is cap-closed-yielding SemiringFamily of X
let X be non-empty n -element FinSequence; :: thesis: for S being SemialgebraFamily of X holds S is cap-closed-yielding SemiringFamily of X
let S be SemialgebraFamily of X; :: thesis: S is cap-closed-yielding SemiringFamily of X
A1: now :: thesis: for i being Nat st i in Seg n holds
S . i is semiring_of_sets of (X . i)
let i be Nat; :: thesis: ( i in Seg n implies S . i is semiring_of_sets of (X . i) )
assume i in Seg n ; :: thesis: S . i is semiring_of_sets of (X . i)
then S . i is semialgebra_of_sets of X . i by Def2;
hence S . i is semiring_of_sets of (X . i) by SRINGS_3:9; :: thesis: verum
end;
for i being Nat st i in Seg n holds
S . i is cap-closed by Def2;
hence S is cap-closed-yielding SemiringFamily of X by A1, SRINGS_4:def 3, SRINGS_4:def 5; :: thesis: verum