let G be strict Group; :: thesis: for b being Element of G holds
( ( for a being Element of G ex i being Integer st a = b |^ i ) iff G = gr {b} )
let b be Element of G; :: thesis: ( ( for a being Element of G ex i being Integer st a = b |^ i ) iff G = gr {b} )
thus ( ( for a being Element of G ex i being Integer st a = b |^ i ) implies G = gr {b} ) :: thesis: ( G = gr {b} implies for a being Element of G ex i being Integer st a = b |^ i )
proof
assume A1: for a being Element of G ex i being Integer st a = b |^ i ; :: thesis: G = gr {b}
for a being Element of G holds a in gr {b}
proof
let a be Element of G; :: thesis: a in gr {b}
ex i being Integer st a = b |^ i by A1;
hence a in gr {b} by GR_CY_1:5; :: thesis: verum
end;
hence G = gr {b} by GROUP_2:62; :: thesis: verum
end;
assume A2: G = gr {b} ; :: thesis: for a being Element of G ex i being Integer st a = b |^ i
let a be Element of G; :: thesis: ex i being Integer st a = b |^ i
a in gr {b} by A2, STRUCT_0:def 5;
hence ex i being Integer st a = b |^ i by GR_CY_1:5; :: thesis: verum