reconsider g = seqIntersection (X,f) as SetSequence of Omega ;
let z be object ; :: thesis: ( z in Union (seqIntersection (X,f)) implies z in X /\ (Union f) )
assume z in Union (seqIntersection (X,f)) ; :: thesis: z in X /\ (Union f)
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: verum

let z be object ; :: thesis: ( z in X /\ (Union f) implies z in Union (seqIntersection (X,f)) )
assume A11: z in X /\ (Union f) ; :: thesis: z in Union (seqIntersection (X,f))
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: verum