let g be Element of X; :: thesis: ( g = x |^ n iff g = (BCI-power X) . (x,n) )
|.n.| = n by ABSVALUE:def 1;
hence ( g = x |^ n iff g = (BCI-power X) . (x,n) ) by Def2; :: thesis: verum