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 V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

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 V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

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 V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

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 V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

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 V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

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 V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

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 V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

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

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V )

assume that

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

A2: <.cB1.) = cF1 and

A3: <.cB2.) = cF2 ; :: thesis: for V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

reconsider FF = filter_image (f,<.cF1,cF2.)) as Filter of the carrier of Y ;

let V be Subset of Y; :: thesis: ( V is open & x in V implies ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V )

assume that

A4: V is open and

A5: x in V ; :: thesis: ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

V in { M where M is Subset of Y : f " M in <.cF1,cF2.) } by A1, A4, A5, CARDFIL2:80, WAYBEL_7:def 5;

then consider M being Subset of Y such that

A6: V = M and

A7: f " M in <.cF1,cF2.) ;

<.cF1,cF2.) = <.[:cB1,cB2:].) by A2, A3, Def1;

then consider B being Element of [:cB1,cB2:] such that

A8: B c= f " M by A7, CARDFIL2:def 8;

B in [:cB1,cB2:] ;

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

A9: B = [:B1,B2:] ;

take B1 ; :: thesis: ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

take B2 ; :: thesis: f .: [:B1,B2:] c= V

A10: f .: [:B1,B2:] c= f .: (f " M) by A8, A9, RELAT_1:123;

f .: (f " M) c= M by FUNCT_1:75;

hence f .: [:B1,B2:] c= V by A6, A10; :: 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 V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

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 V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

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 V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

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 V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

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 V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

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 V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

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 V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

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

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V )

assume that

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

A2: <.cB1.) = cF1 and

A3: <.cB2.) = cF2 ; :: thesis: for V being Subset of Y st V is open & x in V holds

ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

reconsider FF = filter_image (f,<.cF1,cF2.)) as Filter of the carrier of Y ;

let V be Subset of Y; :: thesis: ( V is open & x in V implies ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V )

assume that

A4: V is open and

A5: x in V ; :: thesis: ex B1 being Element of cB1 ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

V in { M where M is Subset of Y : f " M in <.cF1,cF2.) } by A1, A4, A5, CARDFIL2:80, WAYBEL_7:def 5;

then consider M being Subset of Y such that

A6: V = M and

A7: f " M in <.cF1,cF2.) ;

<.cF1,cF2.) = <.[:cB1,cB2:].) by A2, A3, Def1;

then consider B being Element of [:cB1,cB2:] such that

A8: B c= f " M by A7, CARDFIL2:def 8;

B in [:cB1,cB2:] ;

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

A9: B = [:B1,B2:] ;

take B1 ; :: thesis: ex B2 being Element of cB2 st f .: [:B1,B2:] c= V

take B2 ; :: thesis: f .: [:B1,B2:] c= V

A10: f .: [:B1,B2:] c= f .: (f " M) by A8, A9, RELAT_1:123;

f .: (f " M) c= M by FUNCT_1:75;

hence f .: [:B1,B2:] c= V by A6, A10; :: thesis: verum