let x be Element of F_Complex ; :: thesis: for n being Element of NAT ex f being Function of COMPLEX ,COMPLEX st
( f = FPower x,n & FPower x,(n + 1) = f (#) (id COMPLEX ) )
let n be Element of 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

let y be Element of F_Complex ; :: thesis: g . y = x * ((power F_Complex ) . 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 by FUNCT_1:35
.= (x * ((power F_Complex ) . y,n)) * y by Def11
.= x * (((power F_Complex ) . y,n) * y)
.= x * ((power F_Complex ) . y,(n + 1)) by GROUP_1:def 8 ; :: thesis: verum

end;

hence FPower x,(n + 1) = f (#) (id COMPLEX ) by Def11; :: thesis: verum