let n be Nat; :: thesis: for x being object
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds
( x in (Partial_Union XSeq) . n iff ex k being Nat st
( k <= n & x in XSeq . k ) )
let x be object ; :: thesis: for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds
( x in (Partial_Union XSeq) . n iff ex k being Nat st
( k <= n & x in XSeq . k ) )
let X be set ; :: thesis: for Si being SigmaField of X
for XSeq being SetSequence of Si holds
( x in (Partial_Union XSeq) . n iff ex k being Nat st
( k <= n & x in XSeq . k ) )
let Si be SigmaField of X; :: thesis: for XSeq being SetSequence of Si holds
( x in (Partial_Union XSeq) . n iff ex k being Nat st
( k <= n & x in XSeq . k ) )
let XSeq be SetSequence of Si; :: thesis: ( x in (Partial_Union XSeq) . n iff ex k being Nat st
( k <= n & x in XSeq . k ) )
reconsider XSeq = XSeq as SetSequence of X ;
( x in (Partial_Union XSeq) . n iff ex k being Nat st
( k <= n & x in XSeq . k ) ) by Th13;
hence ( x in (Partial_Union XSeq) . n iff ex k being Nat st
( k <= n & x in XSeq . k ) ) ; :: thesis: verum