thus 2 to_power 5 = 2 to_power (3 + 2)
.= (2 to_power 3) * (2 to_power 2) by Th32
.= 32 by Th68, Th69 ; :: thesis: verum