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}

b in Gr

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

for b being Element of G st b in gr {a} holds
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;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

b in Gr

proof

hence
gr {a} = gr {a1}
by A2, GROUP_2:60; :: thesis: verum
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;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