consider cB being basis of (Frechet_Filter NAT) such that
A1:
cB = base_of_frechet_filter
and
[:cB,cB:] is basis of <.(Frechet_Filter NAT),(Frechet_Filter NAT).)
by Th33;
<.(# [:cB,cB:]).] = <.[:base_of_frechet_filter,base_of_frechet_filter:].)
proof
set cF1 =
<.(# [:cB,cB:]).];
set cF2 =
<.[:base_of_frechet_filter,base_of_frechet_filter:].);
now for x being object st x in <.(# [:cB,cB:]).] holds
x in <.[:base_of_frechet_filter,base_of_frechet_filter:].)let x be
object ;
( x in <.(# [:cB,cB:]).] implies x in <.[:base_of_frechet_filter,base_of_frechet_filter:].) )assume A2:
x in <.(# [:cB,cB:]).]
;
x in <.[:base_of_frechet_filter,base_of_frechet_filter:].)then reconsider y =
x as
Subset of
[:NAT,NAT:] ;
consider b being
Element of
# [:cB,cB:] such that A3:
b c= y
by A2, CARDFIL2:def 8;
consider cB3,
cB4 being
filter_base of
NAT such that A4:
cB = cB3
and A5:
cB = cB4
and A6:
[:cB,cB:] = [:cB3,cB4:]
by Def2;
b in { [:B1,B2:] where B1 is Element of cB3, B2 is Element of cB4 : verum }
by A6;
then consider B1 being
Element of
cB3,
B2 being
Element of
cB4 such that A7:
b = [:B1,B2:]
;
b in [:base_of_frechet_filter,base_of_frechet_filter:]
by A1, A4, A5, A7;
hence
x in <.[:base_of_frechet_filter,base_of_frechet_filter:].)
by A3, CARDFIL2:def 8;
verum end;
then A8:
<.(# [:cB,cB:]).] c= <.[:base_of_frechet_filter,base_of_frechet_filter:].)
;
now for x being object st x in <.[:base_of_frechet_filter,base_of_frechet_filter:].) holds
x in <.(# [:cB,cB:]).]let x be
object ;
( x in <.[:base_of_frechet_filter,base_of_frechet_filter:].) implies x in <.(# [:cB,cB:]).] )assume A9:
x in <.[:base_of_frechet_filter,base_of_frechet_filter:].)
;
x in <.(# [:cB,cB:]).]then reconsider y =
x as
Subset of
[:NAT,NAT:] ;
consider b being
Element of
[:base_of_frechet_filter,base_of_frechet_filter:] such that A10:
b c= y
by A9, CARDFIL2:def 8;
ex
cB3,
cB4 being
filter_base of
NAT st
(
cB = cB3 &
cB = cB4 &
[:cB,cB:] = [:cB3,cB4:] )
by Def2;
hence
x in <.(# [:cB,cB:]).]
by A1, A10, CARDFIL2:def 8;
verum end;
then
<.[:base_of_frechet_filter,base_of_frechet_filter:].) c= <.(# [:cB,cB:]).]
;
hence
<.(# [:cB,cB:]).] = <.[:base_of_frechet_filter,base_of_frechet_filter:].)
by A8;
verum
end;
hence
<.[:base_of_frechet_filter,base_of_frechet_filter:].) = <.(Frechet_Filter NAT),(Frechet_Filter NAT).)
by CARDFIL2:21; verum