for TG being commutative TopologicalGroup
for U being a_neighborhood of 1_ TG holds element_left_uniformity U = element_right_uniformity U