theorem Th26: :: POWER:26

for a being Real holds 1 to_power a = 1