thus 2 to_power 3 = 2 to_power (2 + 1)
.= (2 to_power 2) * (2 to_power 1) by Th32
.= 4 * 2 by Th30, Th68
.= 8 ; :: thesis: verum