let n be Element of NAT ; :: thesis: for a being non empty real number holds (a to_power n) to_power 2 = a to_power (2 * n)
let a be non empty real number ; :: thesis: (a to_power n) to_power 2 = a to_power (2 * n)
(a to_power n) to_power 2 = (a to_power n) to_power (1 + 1)
.= ((a to_power n) to_power 1) * ((a to_power n) to_power 1) by FIB_NUM2:7
.= (a to_power n) * ((a to_power n) to_power 1) by POWER:30
.= (a to_power n) * (a to_power n) by POWER:30
.= a to_power (n + n) by FIB_NUM2:7
.= a to_power (2 * n) ;
hence (a to_power n) to_power 2 = a to_power (2 * n) ; :: thesis: verum