let X be set ; :: thesis: for A being Subset of X
for B being SetSequence of X st ( for n being Element of 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 Element of NAT holds B . n = A ) holds
Union B = A
let B be SetSequence of X; :: thesis: ( ( for n being Element of NAT holds B . n = A ) implies Union B = A )
assume A1: for n being Element of NAT holds B . n = A ; :: thesis: Union B = A

now

let x be set ; :: thesis: ( x in rng B implies x = A )
assume x in rng B ; :: thesis: x = A
then ex n being Element of NAT st x = B . n by Th4;
hence x = A by A1; :: thesis: verum

end;

then rng B = {A} by ZFMISC_1:41;
then union (rng B) = A by ZFMISC_1:31;
hence Union B = A by CARD_3:def 4; :: thesis: verum