let n be Element of NAT ; :: thesis: for a being non zero Real holds (a to_power n) to_power 2 = a to_power (2 * n)
let a be non zero Real; :: 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:5
.= (a to_power n) * ((a to_power n) to_power 1) by POWER:25
.= (a to_power n) * (a to_power n) by POWER:25
.= a to_power (n + n) by FIB_NUM2:5
.= a to_power (2 * n) ;
hence (a to_power n) to_power 2 = a to_power (2 * n) ; :: thesis: verum