let G be strict addGroup; :: thesis: Normalizer ((0). G) = G
(0). G is normal Subgroup of G by Th114;
hence Normalizer ((0). G) = G by Th137; :: thesis: verum