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 Th61;
Union ASeq = Union FSi by A1, Th60;
hence Union FSi in Si by PROB_1:46; :: thesis: verum