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

let q be set ; :: thesis:
assume q in Y-section ((union (rng F)),p) ; :: thesis:
then consider x1 being Element of X such that
A3: ( q = x1 & [x1,p] in union (rng F) ) ;
consider T being set such that
A4: ( [x1,p] 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;
Fx . m = Y-section ((F . m),p) by A2;
then ( q in Fx . m & Fx . m in rng Fx ) by A3, A4, A5, FUNCT_2:112;
hence q in union (rng Fx) by TARSKI:def 4; :: thesis:

end;

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

end;