let G be Group; :: thesis: for a being Element of G holds a in gr {a}

let a be Element of G; :: thesis: a in gr {a}

ex i being Integer st a = a |^ i

let a be Element of G; :: thesis: a in gr {a}

ex i being Integer st a = a |^ i

proof

hence
a in gr {a}
by GR_CY_1:5; :: thesis: verum
reconsider i = 1 as Integer ;

take i ; :: thesis: a = a |^ i

thus a = a |^ i by GROUP_1:26; :: thesis: verum

end;take i ; :: thesis: a = a |^ i

thus a = a |^ i by GROUP_1:26; :: thesis: verum