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

for B being SetSequence of X st ( for n being Nat holds B . n = A ) holds

Union B = A

let A be Subset of X; :: thesis: for B being SetSequence of X st ( for n being Nat holds B . n = A ) holds

Union B = A

let B be SetSequence of X; :: thesis: ( ( for n being Nat holds B . n = A ) implies Union B = A )

assume A1: for n being Nat holds B . n = A ; :: thesis: Union B = A

then union (rng B) = A by ZFMISC_1:25;

hence Union B = A by CARD_3:def 4; :: thesis: verum

for B being SetSequence of X st ( for n being Nat holds B . n = A ) holds

Union B = A

let A be Subset of X; :: thesis: for B being SetSequence of X st ( for n being Nat holds B . n = A ) holds

Union B = A

let B be SetSequence of X; :: thesis: ( ( for n being Nat holds B . n = A ) implies Union B = A )

assume A1: for n being Nat holds B . n = A ; :: thesis: Union B = A

now :: thesis: for x being object st x in rng B holds

x = A

then
rng B = {A}
by ZFMISC_1:35;x = A

let x be object ; :: thesis: ( x in rng B implies x = A )

assume x in rng B ; :: thesis: x = A

then ex n being Nat st x = B . n by Th4;

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

end;assume x in rng B ; :: thesis: x = A

then ex n being Nat st x = B . n by Th4;

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

then union (rng B) = A by ZFMISC_1:25;

hence Union B = A by CARD_3:def 4; :: thesis: verum