let n be Nat; :: thesis:
let r be Element of F_Real; :: thesis:
reconsider f = FPower (r,n) as Function of REAL,REAL ;
reconsider g = f (#) (id REAL) as Function of F_Real,F_Real ;

let y be Element of F_Real; :: thesis:
reconsider y1 = y as Element of REAL ;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
thus g . y = (f . y1) * ((id REAL) . y1) by VALUED_1:5
.= (r * (power (y,n))) * y by POLYNOM5:def 12
.= r * (((power F_Real) . (y,n1)) * y)
.= r * (power (y,(n + 1))) by GROUP_1:def 7 ; :: thesis:

end;