let n be non zero Nat; :: thesis: for X being non-empty n -element FinSequence
for S being SemiringFamily of X
for i being Nat st i in Seg n holds
union (S . i) c= X . i
let X be non-empty n -element FinSequence; :: thesis: for S being SemiringFamily of X
for i being Nat st i in Seg n holds
union (S . i) c= X . i
let S be SemiringFamily of X; :: thesis: for i being Nat st i in Seg n holds
union (S . i) c= X . i
let i be Nat; :: thesis: ( i in Seg n implies union (S . i) c= X . i )
assume i in Seg n ; :: thesis: union (S . i) c= X . i
then S . i is semiring_of_sets of (X . i) by Def2;
then union (S . i) c= union (bool (X . i)) by ZFMISC_1:77;
hence union (S . i) c= X . i by ZFMISC_1:81; :: thesis: verum