let n be Nat; :: thesis: for r being Element of F_Real holds power (r,n) = (#Z n) . r
let r be Element of F_Real; :: thesis: power (r,n) = (#Z n) . r
thus power (r,n) = (1. F_Real) * (power (r,n))
.= (FPower ((1. F_Real),n)) . r by POLYNOM5:def 12
.= (#Z n) . r by Th40 ; :: thesis: verum