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 ((meet (rng F)),p) ; :: thesis:
then consider y1 being Element of X such that
A3: ( q = y1 & [y1,p] in meet (rng F) ) ;
for T being set st T in rng Fx holds
q in T

let T be set ; :: thesis:
assume T in rng Fx ; :: thesis:
then consider n being object such that
B1: ( n in dom Fx & T = Fx . n ) by FUNCT_1:def 3;
reconsider n = n as Element of NAT by B1;
dom F = NAT by FUNCT_2:def 1;
then F . n in rng F by FUNCT_1:3;
then [q,p] in F . n by A3, SETFAM_1:def 1;
then q in Y-section ((F . n),p) by A3;
hence q in T by B1, A2; :: thesis:

end;

end;

let T be set ; :: thesis:
assume T in rng F ; :: thesis:
then consider n being object such that
B2: ( n in dom F & T = F . n ) by FUNCT_1:def 3;
reconsider n = n as Nat by B2;
dom Fx = NAT by FUNCT_2:def 1;
then Fx . n in rng Fx by B2, FUNCT_1:3;
then q in Fx . n by B0, SETFAM_1:def 1;
then q in Y-section ((F . n),p) by A2;
then ex y being Element of X st
( q = y & [y,p] in F . n ) ;
hence [q,p] in T by B2; :: thesis:

end;

end;