let g be Element of G; :: thesis: ( g = g |^ n iff g = (power G) . (g,n) )
|.n.| = n by ABSVALUE:def 1;
hence ( g = g |^ n iff g = (power G) . (g,n) ) by Def5; :: thesis: verum