thus 2 to_power 4 = 2 to_power (2 + 2)
.= (2 to_power 2) * (2 to_power 2) by Th32
.= 16 by Th68 ; :: thesis: verum