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 X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1)

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 X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1)

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 X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ) holds
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1)

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

let f be Function of [:X1,X2:],Y; :: thesis: ( ( for x being Element of X1 holds lim_filter ((ProjMap1 (f,x)),cF2) <> {} ) implies lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1) )
assume A1: for x1 being Element of X1 holds lim_filter ((ProjMap1 (f,x1)),cF2) <> {} ; :: thesis: lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1)
now :: thesis: for y0 being object st y0 in lim_filter (f,<.cF1,cF2.)) holds
y0 in lim_filter ((lim_in_cod2 (f,cF2)),cF1)
let y0 be object ; :: thesis: ( y0 in lim_filter (f,<.cF1,cF2.)) implies y0 in lim_filter ((lim_in_cod2 (f,cF2)),cF1) )
assume A2: y0 in lim_filter (f,<.cF1,cF2.)) ; :: thesis: y0 in lim_filter ((lim_in_cod2 (f,cF2)),cF1)
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 B1 holds lim_filter ((ProjMap1 (f,z)),cF2) 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 B1 holds lim_filter ((ProjMap1 (f,z)),cF2) 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 B1 holds lim_filter ((ProjMap1 (f,z)),cF2) c= Cl (Int U)

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

take B2 ; :: thesis: for z being Element of B1 holds lim_filter ((ProjMap1 (f,z)),cF2) c= Cl (Int U)
thus for z being Element of B1 holds lim_filter ((ProjMap1 (f,z)),cF2) c= Cl (Int U) by A6; :: thesis: verum
end;
NeighborhoodSystem y c= filter_image ((lim_in_cod2 (f,cF2)),cF1)
proof
let n be object ; :: according to TARSKI:def 3 :: thesis: ( not n in NeighborhoodSystem y or n in filter_image ((lim_in_cod2 (f,cF2)),cF1) )
assume n in NeighborhoodSystem y ; :: thesis: n in filter_image ((lim_in_cod2 (f,cF2)),cF1)
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 B1 holds lim_filter ((ProjMap1 (f,z)),cF2) 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: ( B1 c= (lim_in_cod2 (f,cF2)) " n1 & (lim_in_cod2 (f,cF2)) " n1 is Subset of X1 )
(lim_in_cod2 (f,cF2)) .: B1 c= n1
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in (lim_in_cod2 (f,cF2)) .: B1 or t in n1 )
assume t in (lim_in_cod2 (f,cF2)) .: B1 ; :: thesis: t in n1
then consider u being object such that
A14: u in dom (lim_in_cod2 (f,cF2)) and
A15: u in B1 and
A16: t = (lim_in_cod2 (f,cF2)) . u by FUNCT_1:def 6;
reconsider u1 = u as Element of X1 by A14;
{t} = lim_filter ((ProjMap1 (f,u1)),cF2) by ;
then A17: t in lim_filter ((ProjMap1 (f,u1)),cF2) by TARSKI:def 1;
lim_filter ((ProjMap1 (f,u1)),cF2) c= Cl (Int Q) by ;
hence t in n1 by A7, A17, A13, A12, A9; :: thesis: verum
end;
hence B1 c= (lim_in_cod2 (f,cF2)) " n1 by FUNCT_2:95; :: thesis: (lim_in_cod2 (f,cF2)) " n1 is Subset of X1
dom (lim_in_cod2 (f,cF2)) = X1 by FUNCT_2:def 1;
hence (lim_in_cod2 (f,cF2)) " n1 is Subset of X1 by RELAT_1:132; :: thesis: verum
end;
then (lim_in_cod2 (f,cF2)) " n1 in cF1 by ;
hence n in filter_image ((lim_in_cod2 (f,cF2)),cF1) ; :: thesis: verum
end;
then filter_image ((lim_in_cod2 (f,cF2)),cF1) is_filter-finer_than NeighborhoodSystem y ;
hence y0 in lim_filter ((lim_in_cod2 (f,cF2)),cF1) ; :: thesis: verum
end;
hence lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1) ; :: thesis: verum