let a be Real; :: thesis: for n being Nat holds |.a.| to_power n = |.(a to_power n).|
let n be Nat; :: thesis: |.a.| to_power n = |.(a to_power n).|

per cases ( a <> 0 or a = 0 ) ;

suppose A1: a <> 0 ; :: thesis: |.a.| to_power n = |.(a to_power n).|

then A2: |.a.| > 0 by COMPLEX1:47;

now :: thesis: |.a.| to_power n = |.(a to_power n).|

per cases ( a > 0 or a < 0 ) by A1;

suppose a > 0 ; :: thesis: |.a.| to_power n = |.(a to_power n).|

then ( a to_power n = |.a.| to_power n & a to_power n > 0 ) by ABSVALUE:def 1, POWER:34;
hence |.a.| to_power n = |.(a to_power n).| by ABSVALUE:def 1; :: thesis: verum

end;

suppose A3: a < 0 ; :: thesis: |.a.| to_power n = |.(a to_power n).|

reconsider m = n as Integer ;

now :: thesis: |.a.| to_power n = |.(a to_power n).|

per cases ( m is even or m is odd ) ;

suppose A4: m is even ; :: thesis: |.a.| to_power n = |.(a to_power n).|

A5: |.a.| to_power n > 0 by A2, POWER:34;
|.a.| to_power n = (- a) to_power m by A3, ABSVALUE:def 1
.= a to_power m by A4, POWER:47 ;
hence |.a.| to_power n = |.(a to_power n).| by A5, ABSVALUE:def 1; :: thesis: verum

end;

suppose A6: m is odd ; :: thesis: |.a.| to_power n = |.(a to_power n).|

A7: |.a.| to_power n > 0 by A2, POWER:34;
|.a.| to_power n = (- a) to_power m by A3, ABSVALUE:def 1
.= - (a to_power m) by A6, POWER:48 ;
hence |.a.| to_power n = |.(- (a to_power n)).| by A7, ABSVALUE:def 1
.= |.(a to_power n).| by COMPLEX1:52 ;
:: thesis: verum

end;

end;

end;

hence |.a.| to_power n = |.(a to_power n).| ; :: thesis: verum

end;

end;

end;

hence |.a.| to_power n = |.(a to_power n).| ; :: thesis: verum

end;

suppose A8: a = 0 ; :: thesis: |.a.| to_power n = |.(a to_power n).|

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: |.a.| to_power n = |.(a to_power n).|

then a to_power n = 1 by NEWTON:4;
hence |.a.| to_power n = |.(a to_power n).| by A8, COMPLEX1:44, COMPLEX1:48; :: thesis: verum

end;

suppose n > 0 ; :: thesis: |.a.| to_power n = |.(a to_power n).|

then |.a.| to_power n = 0 by A8, COMPLEX1:44, POWER:def 2;
hence |.a.| to_power n = |.(a to_power n).| by A8, COMPLEX1:44; :: thesis: verum

end;

end;

end;

end;