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
now :: thesis: for x being object st x in rng B holds
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;
then rng B = {A} by ZFMISC_1:35;
then union (rng B) = A by ZFMISC_1:25;
hence Union B = A by CARD_3:def 4; :: thesis: verum