theorem Th2: :: SERIES_1:2
for a being Real
for n being Nat holds |.a.| to_power n = |.(a to_power n).|