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

now :: thesis: for y being Element of F_Real holds g . y = r * (power (y,(n + 1)))

let y be Element of F_Real; :: thesis: g . y = r * (power (y,(n + 1)))
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: verum

end;

hence FPower (r,(n + 1)) = (FPower (r,n)) (#) (id REAL) by POLYNOM5:def 12; :: thesis: verum