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