now ( dom <.gen_R^1.] = dom the BNbd of FMT_R^1 & ( for x being object st x in dom <.gen_R^1.] holds
<.gen_R^1.] . x = the BNbd of FMT_R^1 . x ) )
the
carrier of
FMT_R^1 = REAL
by TOPMETR:17, FINTOPO7:def 15;
then
dom the
BNbd of
FMT_R^1 = REAL
by FUNCT_2:def 1;
hence
dom <.gen_R^1.] = dom the
BNbd of
FMT_R^1
by Th64, FUNCT_2:def 1;
for x being object st x in dom <.gen_R^1.] holds
<.gen_R^1.] . x = the BNbd of FMT_R^1 . xhereby verum
let x be
object ;
( x in dom <.gen_R^1.] implies <.gen_R^1.] . x = the BNbd of FMT_R^1 . x )assume
x in dom <.gen_R^1.]
;
<.gen_R^1.] . x = the BNbd of FMT_R^1 . xthen reconsider y =
x as
Element of the
carrier of
gen_R^1 ;
reconsider z =
y as
Element of
FMT_R^1 ;
A1:
the
BNbd of
FMT_R^1 . z = U_FMT z
by FINTOPO2:def 6;
now ( U_FMT z c= <.(U_FMT y).] & <.(U_FMT y).] c= U_FMT z )now for o being object st o in U_FMT z holds
o in <.(U_FMT y).]let o be
object ;
( o in U_FMT z implies o in <.(U_FMT y).] )assume A2:
o in U_FMT z
;
o in <.(U_FMT y).]then reconsider S =
o as
Subset of
FMT_R^1 ;
S is
a_neighborhood of
z
by A2, FINTOPO7:def 5;
then consider O being
open Subset of
FMT_R^1 such that A3:
z in O
and A4:
O c= S
by FINTOPO7:15;
A5:
NTop2Top FMT_R^1 = R^1
by FINTOPO7:24;
O is
open Subset of
R^1
by A5, Lm9;
then consider r being
Real such that A6:
r > 0
and A7:
].(z - r),(z + r).[ c= O
by A3, FRECHET:8;
consider n being
Nat such that A8:
1
/ n < r
and A9:
n > 0
by A6, FRECHET:36;
A10:
].(z - (1 / n)),(z + (1 / n)).[ c= ].(z - r),(z + r).[
by A8, INTEGRA6:2;
reconsider z9 =
z as
Point of
(TopSpaceMetr RealSpace) by TOPMETR:def 6, FINTOPO7:def 15;
consider zy being
Point of
RealSpace such that A11:
z9 = zy
and A12:
Balls z9 = { (Ball (zy,(1 / n))) where n is Nat : n <> 0 }
by FRECHET:def 1;
A13:
].(z - (1 / n)),(z + (1 / n)).[ = Ball (
zy,
(1 / n))
by A11, FRECHET:7;
consider py being
Point of
(TopSpaceMetr RealSpace) such that A14:
py = y
and A15:
U_FMT y = Balls py
by Th65;
].(z - (1 / n)),(z + (1 / n)).[ in Balls py
by A13, A9, A12, A14;
then reconsider b =
].(z - (1 / n)),(z + (1 / n)).[ as
Element of
U_FMT y by A15;
b c= S
by A10, A7, A4;
hence
o in <.(U_FMT y).]
by CARDFIL2:def 8;
verum end; hence
U_FMT z c= <.(U_FMT y).]
;
<.(U_FMT y).] c= U_FMT znow for o being object st o in <.(U_FMT y).] holds
o in U_FMT zlet o be
object ;
( o in <.(U_FMT y).] implies o in U_FMT z )assume A16:
o in <.(U_FMT y).]
;
o in U_FMT zthen reconsider O =
o as
Subset of
gen_R^1 ;
consider b being
Element of
U_FMT y such that A17:
b c= O
by A16, CARDFIL2:def 8;
reconsider z9 =
z as
Point of
(TopSpaceMetr RealSpace) by FINTOPO7:def 15, TOPMETR:def 6;
consider zy being
Point of
RealSpace such that A18:
z9 = zy
and A19:
Balls z9 = { (Ball (zy,(1 / n))) where n is Nat : n <> 0 }
by FRECHET:def 1;
consider py being
Point of
(TopSpaceMetr RealSpace) such that A20:
py = y
and A21:
U_FMT y = Balls py
by Th65;
b in Balls z9
by A21, A20;
then consider n being
Nat such that A22:
b = Ball (
zy,
(1 / n))
and A23:
n <> 0
by A19;
A24:
].(z - (1 / n)),(z + (1 / n)).[ = Ball (
zy,
(1 / n))
by A18, FRECHET:7;
A25:
n > 0
by NAT_1:3, A23;
0 / n < 1
/ n
by A25, XREAL_1:74;
then
Ball (
zy,
(1 / n)) is
a_neighborhood of
z
by A24, Th58;
then
Ball (
zy,
(1 / n))
in U_FMT z
by FINTOPO7:def 5;
hence
o in U_FMT z
by A22, A17, CARD_FIL:def 1;
verum end; hence
<.(U_FMT y).] c= U_FMT z
;
verum hence
<.gen_R^1.] . x = the
BNbd of
FMT_R^1 . x
by FINTOPO7:def 9, A1;
verum
end;
then
FMT_Space_Str(# the carrier of gen_R^1,<.gen_R^1.] #) = FMT_R^1
by FUNCT_1:2;
hence
gen_filter gen_R^1 = FMT_R^1
by FINTOPO7:def 10; verum