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 set ; :: 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:21;
hence a in the topology of G by A2, PRE_TOPC:def 5; :: 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:16
.= 1_ G by GROUP_1:def 5 ;
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 6;
then 1_ G in W * (a " ) by A7, GROUP_2:34;
then W * (a " ) is a_neighborhood of (1_ G) * ((1_ G) " ) by A6, A5, CONNSP_2:5;
then consider V being open a_neighborhood of 1_ G such that
A8: V * (V " ) c= W * (a " ) by Th55;
consider E being Subset of G such that
A9: E in B and
A10: E c= V by CONNSP_2:6, YELLOW_8:22;
( E is open & E <> {} ) by A9, YELLOW_8:21;
then a * (M " ) meets E by TOPS_1:80;
then consider d being set 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:33;
(d " ) * a = ((d " ) * a) * (1_ G) by GROUP_1:def 5
.= ((d " ) * a) * (m * (m " )) by GROUP_1:def 6
.= (((d " ) * a) * m) * (m " ) by GROUP_1:def 4
.= ((d " ) * d) * (m " ) by A12, GROUP_1:def 4
.= (1_ G) * (m " ) by GROUP_1:def 6
.= m " by GROUP_1:def 5 ;
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 5;
A15: d in E by A11, XBOOLE_0:def 4;
E * (d " ) c= V * (V " )

proof

let q be set ; :: 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:34;
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, XBOOLE_1:1;
then A17: (E * (d " )) * a c= (W * (a " )) * a by Th5;
d * (d " ) = 1_ G by GROUP_1:def 6;
then 1_ G in E * (d " ) by A15, GROUP_2:34;
then a in (E * (d " )) * a by A14, GROUP_2:34;
hence a in I by GROUP_2:40; :: thesis: I c= W
(W * (a " )) * a = W * ((a " ) * a) by GROUP_2:40
.= W * (1_ G) by GROUP_1:def 6
.= W by GROUP_2:43 ;
hence I c= W by A17, GROUP_2:40; :: 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 set ; :: 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