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