thus 2 to_power 5 = 2 to_power (3 + 2)
.= (2 to_power 3) * (2 to_power 2) by Th27
.= 32 by Th60, Th61 ; :: thesis: verum