let X be set ; :: thesis: for Y being non empty set
for p being set
for F being SetSequence of [:X,Y:]
for Fy being SetSequence of Y st ( for n being Nat holds Fy . n = X-section ((F . n),p) ) holds
X-section ((union (rng F)),p) = union (rng Fy)
let Y be non empty set ; :: thesis: for p being set
for F being SetSequence of [:X,Y:]
for Fy being SetSequence of Y st ( for n being Nat holds Fy . n = X-section ((F . n),p) ) holds
X-section ((union (rng F)),p) = union (rng Fy)
let p be set ; :: thesis: for F being SetSequence of [:X,Y:]
for Fy being SetSequence of Y st ( for n being Nat holds Fy . n = X-section ((F . n),p) ) holds
X-section ((union (rng F)),p) = union (rng Fy)
let F be SetSequence of [:X,Y:]; :: thesis: for Fy being SetSequence of Y st ( for n being Nat holds Fy . n = X-section ((F . n),p) ) holds
X-section ((union (rng F)),p) = union (rng Fy)
let Fy be SetSequence of Y; :: thesis: ( ( for n being Nat holds Fy . n = X-section ((F . n),p) ) implies X-section ((union (rng F)),p) = union (rng Fy) )
assume A2: for n being Nat holds Fy . n = X-section ((F . n),p) ; :: thesis: X-section ((union (rng F)),p) = union (rng Fy)

now :: thesis: for q being set st q in X-section ((union (rng F)),p) holds
q in union (rng Fy)

let q be set ; :: thesis: ( q in X-section ((union (rng F)),p) implies q in union (rng Fy) )
assume q in X-section ((union (rng F)),p) ; :: thesis: q in union (rng Fy)
then consider y1 being Element of Y such that
A3: ( q = y1 & [p,y1] in union (rng F) ) ;
consider T being set such that
A4: ( [p,y1] in T & T in rng F ) by A3, TARSKI:def 4;
consider m being Element of NAT such that
A5: T = F . m by A4, FUNCT_2:113;
Fy . m = X-section ((F . m),p) by A2;
then ( q in Fy . m & Fy . m in rng Fy ) by A3, A4, A5, FUNCT_2:112;
hence q in union (rng Fy) by TARSKI:def 4; :: thesis: verum

end;

then A7: X-section ((union (rng F)),p) c= union (rng Fy) ;

now :: thesis: for q being set st q in union (rng Fy) holds
q in X-section ((union (rng F)),p)

let q be set ; :: thesis: ( q in union (rng Fy) implies q in X-section ((union (rng F)),p) )
assume q in union (rng Fy) ; :: thesis: q in X-section ((union (rng F)),p)
then consider T being set such that
A8: ( q in T & T in rng Fy ) by TARSKI:def 4;
consider m being Element of NAT such that
A9: T = Fy . m by A8, FUNCT_2:113;
q in X-section ((F . m),p) by A2, A8, A9;
then consider y1 being Element of Y such that
A10: ( q = y1 & [p,y1] in F . m ) ;
F . m in rng F by FUNCT_2:112;
then [p,y1] in union (rng F) by A10, TARSKI:def 4;
hence q in X-section ((union (rng F)),p) by A10; :: thesis: verum

end;

then union (rng Fy) c= X-section ((union (rng F)),p) ;
hence X-section ((union (rng F)),p) = union (rng Fy) by A7; :: thesis: verum