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

let q be set ; :: thesis:
assume q in X-section ((meet (rng F)),p) ; :: thesis:
then consider y1 being Element of Y such that
A3: ( q = y1 & [p,y1] in meet (rng F) ) ;
for T being set st T in rng Fy holds
q in T

let T be set ; :: thesis:
assume T in rng Fy ; :: thesis:
then consider n being object such that
B1: ( n in dom Fy & T = Fy . 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 [p,q] in F . n by A3, SETFAM_1:def 1;
then q in X-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 Fy = NAT by FUNCT_2:def 1;
then Fy . n in rng Fy by B2, FUNCT_1:3;
then q in Fy . n by B0, SETFAM_1:def 1;
then q in X-section ((F . n),p) by A2;
then ex y being Element of Y st
( q = y & [p,y] in F . n ) ;
hence [p,q] in T by B2; :: thesis:

end;

end;