let G be Group; :: thesis: ( G is commutative Group implies for H being strict Subgroup of G
for a being Element of G holds H |^ a = H )
assume A1: G is commutative Group ; :: thesis: for H being strict Subgroup of G
for a being Element of G holds H |^ a = H
let H be strict Subgroup of G; :: thesis: for a being Element of G holds H |^ a = H
let a be Element of G; :: thesis: H |^ a = H
the carrier of (H |^ a) = ((a ") * H) * a by Th59
.= (H * (a ")) * a by A1, GROUP_2:112
.= H * ((a ") * a) by GROUP_2:107
.= H * (1_ G) by GROUP_1:def 5
.= the carrier of H by GROUP_2:109 ;
hence H |^ a = H by GROUP_2:59; :: thesis: verum