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_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not 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_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not 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_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not x in XSeq . k ) ) )

let Si be SigmaField of X; :: thesis: for XSeq being SetSequence of Si holds

( x in (Partial_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not x in XSeq . k ) ) )

let XSeq be SetSequence of Si; :: thesis: ( x in (Partial_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not x in XSeq . k ) ) )

reconsider XSeq = XSeq as SetSequence of X ;

( x in (Partial_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not x in XSeq . k ) ) ) by Th16;

hence ( x in (Partial_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not x in XSeq . k ) ) ) ; :: thesis: verum

for X being set

for Si being SigmaField of X

for XSeq being SetSequence of Si holds

( x in (Partial_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not 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_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not 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_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not x in XSeq . k ) ) )

let Si be SigmaField of X; :: thesis: for XSeq being SetSequence of Si holds

( x in (Partial_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not x in XSeq . k ) ) )

let XSeq be SetSequence of Si; :: thesis: ( x in (Partial_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not x in XSeq . k ) ) )

reconsider XSeq = XSeq as SetSequence of X ;

( x in (Partial_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not x in XSeq . k ) ) ) by Th16;

hence ( x in (Partial_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds

not x in XSeq . k ) ) ) ; :: thesis: verum