let n be non zero Nat; :: thesis: for X being non-empty n -element FinSequence
for S being ClassicalSemiringFamily of X holds S is cap-closed-yielding SemiringFamily of X
let X be non-empty n -element FinSequence; :: thesis: for S being ClassicalSemiringFamily of X holds S is cap-closed-yielding SemiringFamily of X
let S be ClassicalSemiringFamily of X; :: thesis: S is cap-closed-yielding SemiringFamily of X
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 A1: i in Seg n ; :: thesis: S . i is semiring_of_sets of (X . i)
S . i is cap-closed with_empty_element semi-diff-closed Subset-Family of (X . i) by A1, Def5;
hence S . i is semiring_of_sets of (X . i) by SRINGS_3:9; :: thesis: verum
end;
then reconsider SC = S as SemiringFamily of X by Def2;
for i being Nat st i in Seg n holds
SC . i is cap-closed by Def5;
hence S is cap-closed-yielding SemiringFamily of X by Def4; :: thesis: verum