let n be Nat; :: thesis: #Z n = FPower ((1. F_Real),n)
reconsider f = FPower ((1. F_Real),n) as Function of REAL,REAL ;
#Z n = f

proof

let r be Element of REAL ; :: according to FUNCT_2:def 8 :: thesis: (#Z n) . r = f . r
thus (#Z n) . r = r #Z n by TAYLOR_1:def 1
.= r |^ n by PREPOWER:36
.= (1. F_Real) * (power ((In (r,F_Real)),n)) by Th39
.= f . r by POLYNOM5:def 12 ; :: thesis: verum

end;

hence #Z n = FPower ((1. F_Real),n) ; :: thesis: verum