let X be set ; :: thesis: for A being Subset of X

for B being SetSequence of X st B is constant & the_value_of B = A holds

for n being Nat holds union { (B . k) where k is Nat : n <= k } = A

let A be Subset of X; :: thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds

for n being Nat holds union { (B . k) where k is Nat : n <= k } = A

let B be SetSequence of X; :: thesis: ( B is constant & the_value_of B = A implies for n being Nat holds union { (B . k) where k is Nat : n <= k } = A )

assume A1: ( B is constant & the_value_of B = A ) ; :: thesis: for n being Nat holds union { (B . k) where k is Nat : n <= k } = A

let n be Nat; :: thesis: union { (B . k) where k is Nat : n <= k } = A

set Y = { (B . k) where k is Nat : n <= k } ;

then { (B . k) where k is Nat : n <= k } = {A} by A2, ZFMISC_1:35;

hence union { (B . k) where k is Nat : n <= k } = A by ZFMISC_1:25; :: thesis: verum

for B being SetSequence of X st B is constant & the_value_of B = A holds

for n being Nat holds union { (B . k) where k is Nat : n <= k } = A

let A be Subset of X; :: thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds

for n being Nat holds union { (B . k) where k is Nat : n <= k } = A

let B be SetSequence of X; :: thesis: ( B is constant & the_value_of B = A implies for n being Nat holds union { (B . k) where k is Nat : n <= k } = A )

assume A1: ( B is constant & the_value_of B = A ) ; :: thesis: for n being Nat holds union { (B . k) where k is Nat : n <= k } = A

let n be Nat; :: thesis: union { (B . k) where k is Nat : n <= k } = A

set Y = { (B . k) where k is Nat : n <= k } ;

A2: now :: thesis: for x being object st x in { (B . k) where k is Nat : n <= k } holds

x = A

{ (B . k) where k is Nat : n <= k } <> {}
by Th1;x = A

let x be object ; :: thesis: ( x in { (B . k) where k is Nat : n <= k } implies x = A )

assume x in { (B . k) where k is Nat : n <= k } ; :: thesis: x = A

then ex k being Nat st

( x = B . k & n <= k ) ;

hence x = A by A1, Lm2; :: thesis: verum

end;assume x in { (B . k) where k is Nat : n <= k } ; :: thesis: x = A

then ex k being Nat st

( x = B . k & n <= k ) ;

hence x = A by A1, Lm2; :: thesis: verum

then { (B . k) where k is Nat : n <= k } = {A} by A2, ZFMISC_1:35;

hence union { (B . k) where k is Nat : n <= k } = A by ZFMISC_1:25; :: thesis: verum