theorem Th46: :: POWER:46

for a being Real holds a to_power 2 = a ^2