theorem :: UNIFORM3:25

for TG being commutative TopologicalGroup holds left_uniformity TG = right_uniformity TG