let X1, X2 be non empty set ; :: thesis: for cB1 being filter_base of X1

for cB2 being filter_base of X2

for cF1 being Filter of X1

for cF2 being Filter of X2

for Y being non empty TopSpace

for x being Point of Y

for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds

for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let cB1 be filter_base of X1; :: thesis: for cB2 being filter_base of X2

for cF1 being Filter of X1

for cF2 being Filter of X2

for Y being non empty TopSpace

for x being Point of Y

for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds

for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let cB2 be filter_base of X2; :: thesis: for cF1 being Filter of X1

for cF2 being Filter of X2

for Y being non empty TopSpace

for x being Point of Y

for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds

for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let cF1 be Filter of X1; :: thesis: for cF2 being Filter of X2

for Y being non empty TopSpace

for x being Point of Y

for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds

for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let cF2 be Filter of X2; :: thesis: for Y being non empty TopSpace

for x being Point of Y

for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds

for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let Y be non empty TopSpace; :: thesis: for x being Point of Y

for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds

for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let x be Point of Y; :: thesis: for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds

for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let f be Function of [:X1,X2:],Y; :: thesis: ( x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 implies for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U) )

assume that

A1: x in lim_filter (f,<.cF1,cF2.)) and

A2: <.cB1.) = cF1 and

A3: <.cB2.) = cF2 ; :: thesis: for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let U be a_neighborhood of x; :: thesis: ( U is closed implies ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in 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 X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

then consider B1 being Element of cB1, B2 being Element of cB2 such that

A4: f .: [:B1,B2:] c= Int U by A1, A2, A3, Th75;

take B1 ; :: thesis: ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

take B2 ; :: thesis: for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

A5: for y being Element of B2 holds f .: [:B1,{y}:] c= Int U

for y being Element of Y st y in lim_filter ((ProjMap2 (f,z)),cF1) holds

( filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y )

for y being Element of Y st y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U) ; :: thesis: verum

for cB2 being filter_base of X2

for cF1 being Filter of X1

for cF2 being Filter of X2

for Y being non empty TopSpace

for x being Point of Y

for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds

for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let cB1 be filter_base of X1; :: thesis: for cB2 being filter_base of X2

for cF1 being Filter of X1

for cF2 being Filter of X2

for Y being non empty TopSpace

for x being Point of Y

for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds

for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let cB2 be filter_base of X2; :: thesis: for cF1 being Filter of X1

for cF2 being Filter of X2

for Y being non empty TopSpace

for x being Point of Y

for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds

for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let cF1 be Filter of X1; :: thesis: for cF2 being Filter of X2

for Y being non empty TopSpace

for x being Point of Y

for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds

for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let cF2 be Filter of X2; :: thesis: for Y being non empty TopSpace

for x being Point of Y

for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds

for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let Y be non empty TopSpace; :: thesis: for x being Point of Y

for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds

for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let x be Point of Y; :: thesis: for f being Function of [:X1,X2:],Y st x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 holds

for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let f be Function of [:X1,X2:],Y; :: thesis: ( x in lim_filter (f,<.cF1,cF2.)) & <.cB1.) = cF1 & <.cB2.) = cF2 implies for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U) )

assume that

A1: x in lim_filter (f,<.cF1,cF2.)) and

A2: <.cB1.) = cF1 and

A3: <.cB2.) = cF2 ; :: thesis: for U being a_neighborhood of x st U is closed holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let U be a_neighborhood of x; :: thesis: ( U is closed implies ex B1 being Element of cB1 ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in 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 X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

then consider B1 being Element of cB1, B2 being Element of cB2 such that

A4: f .: [:B1,B2:] c= Int U by A1, A2, A3, Th75;

take B1 ; :: thesis: ex B2 being Element of cB2 st

for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

take B2 ; :: thesis: for z being Element of X2

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

A5: for y being Element of B2 holds f .: [:B1,{y}:] c= Int U

proof

A6:
for z being Element of B2
let y be Element of B2; :: thesis: f .: [:B1,{y}:] c= Int U

[:B1,{y}:] c= [:B1,B2:] by ZFMISC_1:95;

then f .: [:B1,{y}:] c= f .: [:B1,B2:] by RELAT_1:125;

hence f .: [:B1,{y}:] c= Int U by A4; :: thesis: verum

end;[:B1,{y}:] c= [:B1,B2:] by ZFMISC_1:95;

then f .: [:B1,{y}:] c= f .: [:B1,B2:] by RELAT_1:125;

hence f .: [:B1,{y}:] c= Int U by A4; :: thesis: verum

for y being Element of Y st y in lim_filter ((ProjMap2 (f,z)),cF1) holds

( filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y )

proof

for z being Element of B2
let z be Element of B2; :: thesis: for y being Element of Y st y in lim_filter ((ProjMap2 (f,z)),cF1) holds

( filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y )

let y be Element of Y; :: thesis: ( y in lim_filter ((ProjMap2 (f,z)),cF1) implies ( filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y ) )

assume A7: y in lim_filter ((ProjMap2 (f,z)),cF1) ; :: thesis: ( filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y )

filter_image ((ProjMap2 (f,z)),cF1) is Filter of [#] Y by STRUCT_0:def 3;

hence filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) by Th17; :: thesis: ( Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y )

A8: (ProjMap2 (f,z)) " (Int U) is Subset of X1

end;( filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y )

let y be Element of Y; :: thesis: ( y in lim_filter ((ProjMap2 (f,z)),cF1) implies ( filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y ) )

assume A7: y in lim_filter ((ProjMap2 (f,z)),cF1) ; :: thesis: ( filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y )

filter_image ((ProjMap2 (f,z)),cF1) is Filter of [#] Y by STRUCT_0:def 3;

hence filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) by Th17; :: thesis: ( Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y )

A8: (ProjMap2 (f,z)) " (Int U) is Subset of X1

proof

A9:
for z being Element of B2 holds (ProjMap2 (f,z)) .: B1 c= Int U
dom (ProjMap2 (f,z)) = X1
by FUNCT_2:def 1;

hence (ProjMap2 (f,z)) " (Int U) is Subset of X1 by RELAT_1:132; :: thesis: verum

end;hence (ProjMap2 (f,z)) " (Int U) is Subset of X1 by RELAT_1:132; :: thesis: verum

proof

thus
( Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y )
:: thesis: verum
let z be Element of B2; :: thesis: (ProjMap2 (f,z)) .: B1 c= Int U

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in (ProjMap2 (f,z)) .: B1 or t in Int U )

assume t in (ProjMap2 (f,z)) .: B1 ; :: thesis: t in Int U

then consider u being object such that

u in dom (ProjMap2 (f,z)) and

A10: u in B1 and

A11: t = (ProjMap2 (f,z)) . u by FUNCT_1:def 6;

(ProjMap2 (f,z)) . u = f . (u,z) by A10, MESFUNC9:def 7;

then A12: t = f . [u,z] by A11, BINOP_1:def 1;

f .: [:B1,{z}:] c= Int U by A5;

hence t in Int U by VALB; :: thesis: verum

end;let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in (ProjMap2 (f,z)) .: B1 or t in Int U )

assume t in (ProjMap2 (f,z)) .: B1 ; :: thesis: t in Int U

then consider u being object such that

u in dom (ProjMap2 (f,z)) and

A10: u in B1 and

A11: t = (ProjMap2 (f,z)) . u by FUNCT_1:def 6;

(ProjMap2 (f,z)) . u = f . (u,z) by A10, MESFUNC9:def 7;

then A12: t = f . [u,z] by A11, BINOP_1:def 1;

now :: thesis: ( [u,z] in dom f & [u,z] in [:B1,{z}:] )

then VALB:
t in f .: [:B1,{z}:]
by A12, FUNCT_1:def 6;
[u,z] in [:X1,X2:]
by A10, ZFMISC_1:def 2;

hence [u,z] in dom f by FUNCT_2:def 1; :: thesis: [u,z] in [:B1,{z}:]

( z in {z} & u in B1 ) by TARSKI:def 1, A10;

hence [u,z] in [:B1,{z}:] by ZFMISC_1:def 2; :: thesis: verum

end;hence [u,z] in dom f by FUNCT_2:def 1; :: thesis: [u,z] in [:B1,{z}:]

( z in {z} & u in B1 ) by TARSKI:def 1, A10;

hence [u,z] in [:B1,{z}:] by ZFMISC_1:def 2; :: thesis: verum

f .: [:B1,{z}:] c= Int U by A5;

hence t in Int U by VALB; :: thesis: verum

proof

(ProjMap2 (f,z)) .: B1 c= Int U
by A9;

then B1 c= (ProjMap2 (f,z)) " (Int U) by FUNCT_2:95;

then (ProjMap2 (f,z)) " (Int U) in cF1 by A2, A8, CARDFIL2:def 8;

hence Int U in filter_image ((ProjMap2 (f,z)),cF1) ; :: thesis: y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y

thus y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y by A7, Th19; :: thesis: verum

end;then B1 c= (ProjMap2 (f,z)) " (Int U) by FUNCT_2:95;

then (ProjMap2 (f,z)) " (Int U) in cF1 by A2, A8, CARDFIL2:def 8;

hence Int U in filter_image ((ProjMap2 (f,z)),cF1) ; :: thesis: y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y

thus y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y by A7, Th19; :: thesis: verum

for y being Element of Y st y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

proof

hence
for z being Element of X2
let z be Element of B2; :: thesis: for y being Element of Y st y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U)

let y be Element of Y; :: thesis: ( y in lim_filter ((ProjMap2 (f,z)),cF1) implies y in Cl (Int U) )

assume y in lim_filter ((ProjMap2 (f,z)),cF1) ; :: thesis: y in Cl (Int U)

then ( filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y ) by A6;

hence y in Cl (Int U) by YELLOW19:25; :: thesis: verum

end;y in Cl (Int U)

let y be Element of Y; :: thesis: ( y in lim_filter ((ProjMap2 (f,z)),cF1) implies y in Cl (Int U) )

assume y in lim_filter ((ProjMap2 (f,z)),cF1) ; :: thesis: y in Cl (Int U)

then ( filter_image ((ProjMap2 (f,z)),cF1) is proper Filter of (BoolePoset ([#] Y)) & Int U in filter_image ((ProjMap2 (f,z)),cF1) & y is_a_cluster_point_of filter_image ((ProjMap2 (f,z)),cF1),Y ) by A6;

hence y in Cl (Int U) by YELLOW19:25; :: thesis: verum

for y being Element of Y st z in B2 & y in lim_filter ((ProjMap2 (f,z)),cF1) holds

y in Cl (Int U) ; :: thesis: verum