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
Intersection 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
Intersection B = A
let B be SetSequence of X; :: thesis: ( ( for n being Nat holds B . n = A ) implies Intersection B = A )
assume A1: for n being Nat holds B . n = A ; :: thesis: Intersection 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 meet (rng B) = A by SETFAM_1:10;
hence Intersection B = A by Th8; :: thesis: verum