let G be TopologicalGroup; :: thesis: for B being Basis of 1_ G
for M being dense Subset of G holds { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } is Basis of G
let B be Basis of 1_ G; :: thesis: for M being dense Subset of G holds { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } is Basis of G
let M be dense Subset of G; :: thesis: { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } is Basis of G
set Z = { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } ;
A1: { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } c= the topology of G

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } or a in the topology of G )
assume a in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } ; :: thesis: a in the topology of G
then consider V being Subset of G, x being Point of G such that
A2: a = V * x and
A3: V in B and
x in M ;
reconsider V = V as Subset of G ;
V is open by A3, YELLOW_8:12;
hence a in the topology of G by A2, PRE_TOPC:def 2; :: thesis: verum

end;

A4: for W being Subset of G st W is open holds
for a being Point of G st a in W holds
ex V being Subset of G st
( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W )

proof

A5: (1_ G) * ((1_ G) ") = (1_ G) * (1_ G) by GROUP_1:8
.= 1_ G by GROUP_1:def 4 ;
let W be Subset of G; :: thesis: ( W is open implies for a being Point of G st a in W holds
ex V being Subset of G st
( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W ) )
assume A6: W is open ; :: thesis: for a being Point of G st a in W holds
ex V being Subset of G st
( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W )
let a be Point of G; :: thesis: ( a in W implies ex V being Subset of G st
( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W ) )
assume A7: a in W ; :: thesis: ex V being Subset of G st
( V in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in V & V c= W )
1_ G = a * (a ") by GROUP_1:def 5;
then 1_ G in W * (a ") by A7, GROUP_2:28;
then W * (a ") is a_neighborhood of (1_ G) * ((1_ G) ") by A6, A5, CONNSP_2:3;
then consider V being open a_neighborhood of 1_ G such that
A8: V * (V ") c= W * (a ") by Th54;
consider E being Subset of G such that
A9: E in B and
A10: E c= V by CONNSP_2:4, YELLOW_8:13;
( E is open & E <> {} ) by A9, YELLOW_8:12;
then a * (M ") meets E by TOPS_1:45;
then consider d being object such that
A11: d in (a * (M ")) /\ E by XBOOLE_0:4;
reconsider d = d as Point of G by A11;
take I = E * ((d ") * a); :: thesis: ( I in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } & a in I & I c= W )
d in a * (M ") by A11, XBOOLE_0:def 4;
then consider m being Point of G such that
A12: d = a * m and
A13: m in M " by GROUP_2:27;
(d ") * a = ((d ") * a) * (1_ G) by GROUP_1:def 4
.= ((d ") * a) * (m * (m ")) by GROUP_1:def 5
.= (((d ") * a) * m) * (m ") by GROUP_1:def 3
.= ((d ") * d) * (m ") by A12, GROUP_1:def 3
.= (1_ G) * (m ") by GROUP_1:def 5
.= m " by GROUP_1:def 4 ;
then (d ") * a in M by A13, Th7;
hence I in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } by A9; :: thesis: ( a in I & I c= W )
A14: (1_ G) * a = a by GROUP_1:def 4;
A15: d in E by A11, XBOOLE_0:def 4;
E * (d ") c= V * (V ")

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in E * (d ") or q in V * (V ") )
assume q in E * (d ") ; :: thesis: q in V * (V ")
then A16: ex v being Point of G st
( q = v * (d ") & v in E ) by GROUP_2:28;
d " in V " by A10, A15;
hence q in V * (V ") by A10, A16; :: thesis: verum

end;

then E * (d ") c= W * (a ") by A8;
then A17: (E * (d ")) * a c= (W * (a ")) * a by Th5;
d * (d ") = 1_ G by GROUP_1:def 5;
then 1_ G in E * (d ") by A15, GROUP_2:28;
then a in (E * (d ")) * a by A14, GROUP_2:28;
hence a in I by GROUP_2:34; :: thesis: I c= W
(W * (a ")) * a = W * ((a ") * a) by GROUP_2:34
.= W * (1_ G) by GROUP_1:def 5
.= W by GROUP_2:37 ;
hence I c= W by A17, GROUP_2:34; :: thesis: verum

end;

{ (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } c= bool the carrier of G

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } or a in bool the carrier of G )
assume a in { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } ; :: thesis: a in bool the carrier of G
then ex V being Subset of G ex x being Point of G st
( a = V * x & V in B & x in M ) ;
hence a in bool the carrier of G ; :: thesis: verum

end;

hence { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } is Basis of G by A1, A4, YELLOW_9:32; :: thesis: verum