4 to_power 4 = 4 to_power (3 + 1)
.= (4 to_power 3) * (4 to_power 1) by POWER:27
.= (4 to_power (2 + 1)) * 4 by POWER:25
.= ((4 to_power 2) * (4 to_power 1)) * 4 by POWER:27
.= ((4 to_power (1 + 1)) * 4) * 4 by POWER:25
.= (((4 to_power 1) * (4 to_power 1)) * 4) * 4 by POWER:27
.= (((4 to_power 1) * 4) * 4) * 4 by POWER:25
.= ((4 * 4) * 4) * 4 by POWER:25
.= 256 ;
hence 4 to_power 4 = 256 ; :: thesis: verum