let x be Element of F_Complex; :: thesis: for n being Nat ex f being Function of COMPLEX,COMPLEX st
( f = FPower (x,n) & FPower (x,(n + 1)) = f (#) (id COMPLEX) )
let n be Nat; :: thesis: ex f being Function of COMPLEX,COMPLEX st
( f = FPower (x,n) & FPower (x,(n + 1)) = f (#) (id COMPLEX) )
A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
then reconsider f = FPower (x,n) as Function of COMPLEX,COMPLEX ;
reconsider g = f (#) (id COMPLEX) as Function of F_Complex,F_Complex by A1;
take f ; :: thesis: ( f = FPower (x,n) & FPower (x,(n + 1)) = f (#) (id COMPLEX) )
thus f = FPower (x,n) ; :: thesis: FPower (x,(n + 1)) = f (#) (id COMPLEX)
now :: thesis: for y being Element of F_Complex holds g . y = x * (power (y,(n + 1)))
let y be Element of F_Complex; :: thesis: g . y = x * (power (y,(n + 1)))
reconsider y1 = y as Element of COMPLEX by COMPLFLD:def 1;
thus g . y = (f . y1) * ((id COMPLEX) . y1) by VALUED_1:5
.= ((FPower (x,n)) . y) * y
.= (x * (power (y,n))) * y by Def12
.= x * (((power F_Complex) . (y,n)) * y)
.= x * (power (y,(n + 1))) by GROUP_1:def 7 ; :: thesis: verum
end;
hence FPower (x,(n + 1)) = f (#) (id COMPLEX) by Def12; :: thesis: verum