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)

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)

hence
lim_filter (f,<.cF1,cF2.)) c= lim_filter ((lim_in_cod2 (f,cF2)),cF1)
; :: thesis: verumy0 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)

hence y0 in lim_filter ((lim_in_cod2 (f,cF2)),cF1) ; :: thesis: verum

end;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

NeighborhoodSystem y c= filter_image ((lim_in_cod2 (f,cF2)),cF1)
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;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

proof

then
filter_image ((lim_in_cod2 (f,cF2)),cF1) is_filter-finer_than NeighborhoodSystem y
;
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 A10, CONNSP_2:def 1;

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 PRE_TOPC:18, A8, TOPS_1:5;

A13: Cl (Int Q) c= Cl Q by TOPS_1:16, PRE_TOPC:19;

reconsider n1 = n as Subset of Y by A7;

hence n in filter_image ((lim_in_cod2 (f,cF2)),cF1) ; :: thesis: verum

end;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 A10, CONNSP_2:def 1;

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 PRE_TOPC:18, A8, TOPS_1:5;

A13: Cl (Int Q) c= Cl Q by TOPS_1:16, PRE_TOPC:19;

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 )

then
(lim_in_cod2 (f,cF2)) " n1 in cF1
by A3, CARDFIL2:def 8;
(lim_in_cod2 (f,cF2)) .: B1 c= n1

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;proof

hence
B1 c= (lim_in_cod2 (f,cF2)) " n1
by FUNCT_2:95; :: thesis: (lim_in_cod2 (f,cF2)) " n1 is Subset of X1
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 A16, A1, Def7;

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 A11, A15;

hence t in n1 by A7, A17, A13, A12, A9; :: thesis: verum

end;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 A16, A1, Def7;

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 A11, A15;

hence t in n1 by A7, A17, A13, A12, A9; :: thesis: verum

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

hence n in filter_image ((lim_in_cod2 (f,cF2)),cF1) ; :: thesis: verum

hence y0 in lim_filter ((lim_in_cod2 (f,cF2)),cF1) ; :: thesis: verum