let G be Group; :: thesis: for G1 being Subgroup of G
for a being Element of G
for a1 being Element of G1 st a = a1 holds
gr {a} = gr {a1}
let G1 be Subgroup of G; :: thesis: for a being Element of G
for a1 being Element of G1 st a = a1 holds
gr {a} = gr {a1}
let a be Element of G; :: thesis: for a1 being Element of G1 st a = a1 holds
gr {a} = gr {a1}
let a1 be Element of G1; :: thesis: ( a = a1 implies gr {a} = gr {a1} )
reconsider Gr = gr {a1} as Subgroup of G by GROUP_2:56;
assume A1: a = a1 ; :: thesis: gr {a} = gr {a1}
A2: for b being Element of G st b in Gr holds
b in gr {a}

proof

let b be Element of G; :: thesis: ( b in Gr implies b in gr {a} )
assume A3: b in Gr ; :: thesis: b in gr {a}
then b in G1 by GROUP_2:40;
then reconsider b1 = b as Element of G1 by STRUCT_0:def 5;
consider i being Integer such that
A4: b1 = a1 |^ i by A3, GR_CY_1:5;
b = a |^ i by A1, A4, GROUP_4:2;
hence b in gr {a} by GR_CY_1:5; :: thesis: verum

end;

for b being Element of G st b in gr {a} holds
b in Gr

proof

let b be Element of G; :: thesis: ( b in gr {a} implies b in Gr )
assume b in gr {a} ; :: thesis: b in Gr
then consider i being Integer such that
A5: b = a |^ i by GR_CY_1:5;
b = a1 |^ i by A1, A5, GROUP_4:2;
hence b in Gr by GR_CY_1:5; :: thesis: verum

end;

hence gr {a} = gr {a1} by A2, GROUP_2:60; :: thesis: verum