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