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 ;
b = a |^ i by ;
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 ;
hence b in Gr by GR_CY_1:5; :: thesis: verum
end;
hence gr {a} = gr {a1} by ; :: thesis: verum