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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= Int U

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

for y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= Int U

now :: 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 y being Element of B1 holds f .: [:{y},B2:] c= Int U

hence
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 y being Element of B1 holds f .: [:{y},B2:] c= 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 y being Element of B1 holds f .: [:{y},B2:] c= Int U )

assume U is closed ; :: thesis: ex B1 being Element of cB1 ex B2 being Element of cB2 st

for y being Element of B1 holds f .: [:{y},B2:] c= 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 = B1; :: thesis: ex B2 being Element of cB2 st

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

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

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

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

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

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

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

assume U is closed ; :: thesis: ex B1 being Element of cB1 ex B2 being Element of cB2 st

for y being Element of B1 holds f .: [:{y},B2:] c= 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 = B1; :: thesis: ex B2 being Element of cB2 st

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

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

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

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

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

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

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

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