theorem Th6: :: FIB_NUM3:6

for n being Element of NAT
for a being non zero Real holds (a to_power n) to_power 2 = a to_power (2 * n)