let X be set ; :: thesis: for Si being SigmaField of X

for FSi being FinSequence of Si holds Union FSi in Si

let Si be SigmaField of X; :: thesis: for FSi being FinSequence of Si holds Union FSi in Si

let FSi be FinSequence of Si; :: thesis: Union FSi in Si

consider ASeq being SetSequence of Si such that

A1: ( ( for k being Nat st k in dom FSi holds

ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

ASeq . k = {} ) ) by Th56;

reconsider ASeq = ASeq as SetSequence of X ;

( ( for k being Nat st k in dom FSi holds

ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

ASeq . k = {} ) ) by A1;

then Union ASeq = Union FSi by Th55;

hence Union FSi in Si by PROB_1:17; :: thesis: verum

for FSi being FinSequence of Si holds Union FSi in Si

let Si be SigmaField of X; :: thesis: for FSi being FinSequence of Si holds Union FSi in Si

let FSi be FinSequence of Si; :: thesis: Union FSi in Si

consider ASeq being SetSequence of Si such that

A1: ( ( for k being Nat st k in dom FSi holds

ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

ASeq . k = {} ) ) by Th56;

reconsider ASeq = ASeq as SetSequence of X ;

( ( for k being Nat st k in dom FSi holds

ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds

ASeq . k = {} ) ) by A1;

then Union ASeq = Union FSi by Th55;

hence Union FSi in Si by PROB_1:17; :: thesis: verum