let Omega be non empty set ; :: thesis:
let f be SetSequence of Omega; :: thesis:
let X be Subset of Omega; :: thesis:
A1: dom f = NAT by FUNCT_2:def 1;

now :: thesis:

reconsider g = seqIntersection (X,f) as SetSequence of Omega ;
let z be object ; :: thesis:
assume z in Union (seqIntersection (X,f)) ; :: thesis:
then consider u being set such that
A2: z in u and
A3: u in rng g by TARSKI:def 4;
consider v being object such that
A4: v in dom g and
A5: u = g . v by A3, FUNCT_1:def 3;
reconsider n = v as Element of NAT by A4, FUNCT_2:def 1;
A6: z in X /\ (f . n) by A2, A5, Def1;
then A7: z in X by XBOOLE_0:def 4;
A8: f . n in rng f by A1, FUNCT_1:def 3;
z in f . n by A6, XBOOLE_0:def 4;
then z in Union f by A8, TARSKI:def 4;
hence z in X /\ (Union f) by A7, XBOOLE_0:def 4; :: thesis:

end;

then A9: Union (seqIntersection (X,f)) c= X /\ (Union f) ;
A10: dom (seqIntersection (X,f)) = NAT by FUNCT_2:def 1;

now :: thesis:

let z be object ; :: thesis:
assume A11: z in X /\ (Union f) ; :: thesis:
then z in union (rng f) by XBOOLE_0:def 4;
then consider u being set such that
A12: z in u and
A13: u in rng f by TARSKI:def 4;
consider v being object such that
A14: v in dom f and
A15: u = f . v by A13, FUNCT_1:def 3;
reconsider n = v as Element of NAT by A14, FUNCT_2:def 1;
X /\ (f . n) = (seqIntersection (X,f)) . n by Def1;
then A16: X /\ (f . n) in rng (seqIntersection (X,f)) by A10, FUNCT_1:def 3;
z in X by A11, XBOOLE_0:def 4;
then z in X /\ (f . n) by A12, A15, XBOOLE_0:def 4;
hence z in Union (seqIntersection (X,f)) by A16, TARSKI:def 4; :: thesis:

end;

then X /\ (Union f) c= Union (seqIntersection (X,f)) ;
hence X /\ (Union f) = Union (seqIntersection (X,f)) by A9, XBOOLE_0:def 10; :: thesis: