5 to_power 5 = 5 to_power (4 + 1)
.= (5 to_power 4) * (5 to_power 1) by POWER:32
.= (5 to_power (3 + 1)) * 5 by POWER:30
.= ((5 to_power 3) * (5 to_power 1)) * 5 by POWER:32
.= ((5 to_power (2 + 1)) * 5) * 5 by POWER:30
.= (((5 to_power 2) * (5 to_power 1)) * 5) * 5 by POWER:32
.= (((5 to_power (1 + 1)) * 5) * 5) * 5 by POWER:30
.= ((((5 to_power 1) * (5 to_power 1)) * 5) * 5) * 5 by POWER:32
.= ((((5 to_power 1) * 5) * 5) * 5) * 5 by POWER:30
.= (((5 * 5) * 5) * 5) * 5 by POWER:30
.= 3125 ;
hence 5 to_power 5 = 3125 ; :: thesis: verum