thus 2 to_power 2 = 2 ^2 by Th53
.= 4 ; :: thesis: verum