thus 2 to_power 6 = 2 to_power (3 + 3)
.= (2 to_power 3) * (2 to_power 3) by Th27
.= 64 by Th61 ; :: thesis: verum