thus 2 to_power 2 = 2 ^2 by Th46
.= 4 ; :: thesis: