let X1, X2 be non empty set ; :: thesis: for cF1 being Filter of X1
for cF2 being Filter of X2
for Y being non empty Hausdorff regular TopSpace
for f being Function of [:X1,X2:],Y st ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2)

let cF1 be Filter of X1; :: thesis: for cF2 being Filter of X2
for Y being non empty Hausdorff regular TopSpace
for f being Function of [:X1,X2:],Y st ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2)

let cF2 be Filter of X2; :: thesis: for Y being non empty Hausdorff regular TopSpace
for f being Function of [:X1,X2:],Y st ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2)

let Y be non empty Hausdorff regular TopSpace; :: thesis: for f being Function of [:X1,X2:],Y st ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2)

let f be Function of [:X1,X2:],Y; :: thesis: ( ( for x being Element of X2 holds lim_filter ((ProjMap2 (f,x)),cF1) <> {} ) implies lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2) )
assume A1: for x1 being Element of X2 holds lim_filter ((ProjMap2 (f,x1)),cF1) <> {} ; :: thesis: lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2)
now :: thesis: for y0 being object st y0 in lim_filter (f,<.cF1,cF2.)) holds
y0 in lim_filter ((lim_in_cod1 (f,cF1)),cF2)
let y0 be object ; :: thesis: ( y0 in lim_filter (f,<.cF1,cF2.)) implies y0 in lim_filter ((lim_in_cod1 (f,cF1)),cF2) )
assume A2: y0 in lim_filter (f,<.cF1,cF2.)) ; :: thesis: y0 in lim_filter ((lim_in_cod1 (f,cF1)),cF2)
then reconsider y = y0 as Element of Y ;
consider cB1 being filter_base of X1 such that
cB1 = cF1 and
A3: <.cB1.) = cF1 by Th18;
consider cB2 being filter_base of X2 such that
cB2 = cF2 and
A4: <.cB2.) = cF2 by Th18;
A5: for U being a_neighborhood of y st U is closed holds
ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of B2 holds lim_filter ((ProjMap2 (f,z)),cF1) c= Cl (Int U)
proof
let U be a_neighborhood of y; :: thesis: ( U is closed implies ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of B2 holds lim_filter ((ProjMap2 (f,z)),cF1) c= Cl (Int U) )

assume U is closed ; :: thesis: ex B1 being Element of cB1 ex B2 being Element of cB2 st
for z being Element of B2 holds lim_filter ((ProjMap2 (f,z)),cF1) c= Cl (Int U)

then consider B1 being Element of cB1, B2 being Element of cB2 such that
A6: for z being Element of X2
for t being Element of Y st z in B2 & t in lim_filter ((ProjMap2 (f,z)),cF1) holds
t in Cl (Int U) by A3, A4, A2, Th77;
take B1 ; :: thesis: ex B2 being Element of cB2 st
for z being Element of B2 holds lim_filter ((ProjMap2 (f,z)),cF1) c= Cl (Int U)

take B2 ; :: thesis: for z being Element of B2 holds lim_filter ((ProjMap2 (f,z)),cF1) c= Cl (Int U)
thus for z being Element of B2 holds lim_filter ((ProjMap2 (f,z)),cF1) c= Cl (Int U) by A6; :: thesis: verum
end;
NeighborhoodSystem y c= filter_image ((lim_in_cod1 (f,cF1)),cF2)
proof
let n be object ; :: according to TARSKI:def 3 :: thesis: ( not n in NeighborhoodSystem y or n in filter_image ((lim_in_cod1 (f,cF1)),cF2) )
assume n in NeighborhoodSystem y ; :: thesis: n in filter_image ((lim_in_cod1 (f,cF1)),cF2)
then n in { A where A is a_neighborhood of y : verum } by YELLOW19:def 1;
then consider A being a_neighborhood of y such that
A7: n = A ;
y in Int A by CONNSP_2:def 1;
then consider Q being Subset of Y such that
A8: Q is closed and
A9: Q c= A and
A10: y in Int Q by YELLOW_8:27;
Q is a_neighborhood of y by ;
then consider B1 being Element of cB1, B2 being Element of cB2 such that
A11: for z being Element of B2 holds lim_filter ((ProjMap2 (f,z)),cF1) c= Cl (Int Q) by A8, A5;
A12: Cl Q = Q by ;
A13: Cl (Int Q) c= Cl Q by ;
reconsider n1 = n as Subset of Y by A7;
now :: thesis: ( B2 c= (lim_in_cod1 (f,cF1)) " n1 & (lim_in_cod1 (f,cF1)) " n1 is Subset of X2 )
(lim_in_cod1 (f,cF1)) .: B2 c= n1
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in (lim_in_cod1 (f,cF1)) .: B2 or t in n1 )
assume t in (lim_in_cod1 (f,cF1)) .: B2 ; :: thesis: t in n1
then consider u being object such that
A14: u in dom (lim_in_cod1 (f,cF1)) and
A15: u in B2 and
A16: t = (lim_in_cod1 (f,cF1)) . u by FUNCT_1:def 6;
reconsider u1 = u as Element of X2 by A14;
{t} = lim_filter ((ProjMap2 (f,u1)),cF1) by ;
then A17: t in lim_filter ((ProjMap2 (f,u1)),cF1) by TARSKI:def 1;
lim_filter ((ProjMap2 (f,u1)),cF1) c= Cl (Int Q) by ;
hence t in n1 by A7, A17, A13, A12, A9; :: thesis: verum
end;
hence B2 c= (lim_in_cod1 (f,cF1)) " n1 by FUNCT_2:95; :: thesis: (lim_in_cod1 (f,cF1)) " n1 is Subset of X2
dom (lim_in_cod1 (f,cF1)) = X2 by FUNCT_2:def 1;
hence (lim_in_cod1 (f,cF1)) " n1 is Subset of X2 by RELAT_1:132; :: thesis: verum
end;
then (lim_in_cod1 (f,cF1)) " n1 in cF2 by ;
hence n in filter_image ((lim_in_cod1 (f,cF1)),cF2) ; :: thesis: verum
end;
then filter_image ((lim_in_cod1 (f,cF1)),cF2) is_filter-finer_than NeighborhoodSystem y ;
hence y0 in lim_filter ((lim_in_cod1 (f,cF1)),cF2) ; :: thesis: verum
end;
hence lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod1 (f,cF1)),cF2) ; :: thesis: verum