theorem Th24: :: POWER:24

for a being Real holds a to_power 0 = 1