let TG be TopologicalGroup; :: thesis: the topology of (TopSpace_induced_by (right_uniformity TG)) = the topology of TG
set X = the topology of (FMT2TopSpace (FMT_induced_by (right_uniformity TG)));
set Y = the topology of TG;
A2: the topology of (FMT2TopSpace (FMT_induced_by (right_uniformity TG))) c= the topology of TG

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of (FMT2TopSpace (FMT_induced_by (right_uniformity TG))) or x in the topology of TG )
assume x in the topology of (FMT2TopSpace (FMT_induced_by (right_uniformity TG))) ; :: thesis: x in the topology of TG
then x in Family_open_set (FMT_induced_by (right_uniformity TG)) by FINTOPO7:def 16;
then consider y being open Subset of (FMT_induced_by (right_uniformity TG)) such that
A3: x = y ;
reconsider z = x as Subset of TG by A3;
z is open

proof

now :: thesis: for t being Point of TG st t in z holds
ex A being Subset of TG st
( A is a_neighborhood of t & A c= z )

let t be Point of TG; :: thesis: ( t in z implies ex A being Subset of TG st
( A is a_neighborhood of t & A c= z ) )
assume A4: t in z ; :: thesis: ex A being Subset of TG st
( A is a_neighborhood of t & A c= z )
reconsider t1 = t as Point of (FMT_induced_by (right_uniformity TG)) ;
A5: y in U_FMT t1 by A3, A4, FINTOPO7:def 1;
reconsider t2 = t1 as Element of (right_uniformity TG) ;
z in Neighborhood t2 by A3, A5, UNIFORM2:def 14;
then consider V0 being Element of the entourages of (right_uniformity TG) such that
A6: z = Neighborhood (V0,t2) ;
consider tg being Element of system_right_uniformity TG such that
A7: tg c= V0 by CARDFIL2:def 8;
tg in { (element_right_uniformity U) where U is a_neighborhood of 1_ TG : verum } ;
then consider U0 being a_neighborhood of 1_ TG such that
A8: tg = element_right_uniformity U0 ;
reconsider A = U0 * {t} as a_neighborhood of t by Th5;
A c= z

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in A or u in z )
assume u in A ; :: thesis: u in z
then consider u0, u1 being Element of TG such that
A9: u = u0 * u1 and
A10: u0 in U0 and
A11: u1 in {t} ;
reconsider u2 = u as Element of TG by A9;
u0 * (1_ TG) in U0 by A10, GROUP_1:def 4;
then u0 * (t * (t ")) in U0 by GROUP_1:def 5;
then (u0 * t) * (t ") in U0 by GROUP_1:def 3;
then u2 * (t ") in U0 by A9, A11, TARSKI:def 1;
then [t,u2] in element_right_uniformity U0 ;
hence u in z by A6, A7, A8; :: thesis: verum

end;

hence ex A being Subset of TG st
( A is a_neighborhood of t & A c= z ) ; :: thesis: verum

end;

hence z is open by CONNSP_2:7; :: thesis: verum

end;

hence x in the topology of TG ; :: thesis: verum

end;

the topology of TG c= the topology of (FMT2TopSpace (FMT_induced_by (right_uniformity TG)))

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in the topology of TG or u in the topology of (FMT2TopSpace (FMT_induced_by (right_uniformity TG))) )
assume A12: u in the topology of TG ; :: thesis: u in the topology of (FMT2TopSpace (FMT_induced_by (right_uniformity TG)))
then reconsider u = u as Subset of TG ;
reconsider v = u as Subset of (FMT_induced_by (right_uniformity TG)) ;
for x being Element of (FMT_induced_by (right_uniformity TG)) st x in v holds
v in U_FMT x

proof

let x be Element of (FMT_induced_by (right_uniformity TG)); :: thesis: ( x in v implies v in U_FMT x )
assume A13: x in v ; :: thesis: v in U_FMT x
reconsider t2 = x as Element of (right_uniformity TG) ;
reconsider t3 = x as Element of TG ;
reconsider w = v as Subset of TG ;

now :: thesis: ( 1_ TG in w * ({t3} ") & w * ({t3} ") is open )

{(t3 ")} = {t3} " by GROUP_2:3;
then t3 " in {t3} " by TARSKI:def 1;
then t3 * (t3 ") in w * ({t3} ") by A13;
hence 1_ TG in w * ({t3} ") by GROUP_1:def 5; :: thesis: w * ({t3} ") is open
w is open by A12;
hence w * ({t3} ") is open ; :: thesis: verum

end;

then reconsider U0 = w * ({t3} ") as a_neighborhood of 1_ TG by CONNSP_2:6;
element_right_uniformity U0 in system_right_uniformity TG ;
then reconsider V0 = element_right_uniformity U0 as Element of the entourages of (right_uniformity TG) by CARDFIL2:def 8;
v = { y where y is Element of TG : [t2,y] in V0 }

proof

set v2 = { y where y is Element of TG : [t2,y] in V0 } ;
A15: v c= { y where y is Element of TG : [t2,y] in V0 }

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in v or t in { y where y is Element of TG : [t2,y] in V0 } )
assume A16: t in v ; :: thesis: t in { y where y is Element of TG : [t2,y] in V0 }
then reconsider t4 = t as Element of TG ;
{(t3 ")} = {t3} " by GROUP_2:3;
then t3 " in {t3} " by TARSKI:def 1;
then t4 * (t3 ") in w * ({t3} ") by A16;
then [t2,t4] in element_right_uniformity U0 ;
hence t in { y where y is Element of TG : [t2,y] in V0 } ; :: thesis: verum

end;

{ y where y is Element of TG : [t2,y] in V0 } c= v

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { y where y is Element of TG : [t2,y] in V0 } or t in v )
assume t in { y where y is Element of TG : [t2,y] in V0 } ; :: thesis: t in v
then consider y0 being Element of TG such that
A18: t = y0 and
A19: [t2,y0] in V0 ;
consider xt, yt being Element of TG such that
A20: [t2,y0] = [xt,yt] and
A21: yt * (xt ") in U0 by A19;
( t2 = xt & y0 = yt ) by A20, XTUPLE_0:1;
then consider u1, u2 being Element of TG such that
A22: y0 * (t3 ") = u1 * u2 and
A23: u1 in w and
A24: u2 in {t3} " by A21;
{(t3 ")} = {t3} " by GROUP_2:3;
then u2 = t3 " by A24, TARSKI:def 1;
hence t in v by A22, A23, A18, GROUP_1:6; :: thesis: verum

end;

hence v = { y where y is Element of TG : [t2,y] in V0 } by A15; :: thesis: verum

end;

then v = Neighborhood (V0,t2) ;
then v in Neighborhood t2 ;
hence v in U_FMT x by UNIFORM2:def 14; :: thesis: verum

end;

then v is open ;
then u in Family_open_set (FMT_induced_by (right_uniformity TG)) ;
hence u in the topology of (FMT2TopSpace (FMT_induced_by (right_uniformity TG))) by FINTOPO7:def 16; :: thesis: verum

end;

hence the topology of (TopSpace_induced_by (right_uniformity TG)) = the topology of TG by A2; :: thesis: verum