let x be Element of F_Complex ; :: thesis: ex x1 being Element of COMPLEX st
( x = x1 & FPower x,1 = x1 (#) (id COMPLEX ) )
reconsider x1 = x as Element of COMPLEX by COMPLFLD:def 1;
take x1 ; :: thesis: ( x = x1 & FPower x,1 = x1 (#) (id COMPLEX ) )
thus x = x1 ; :: thesis: FPower x,1 = x1 (#) (id COMPLEX )
the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
then reconsider f = x1 (#) (id COMPLEX ) as Function of F_Complex ,F_Complex ;

now

let y be Element of F_Complex ; :: thesis: f . y = x * ((power F_Complex ) . y,1)
reconsider y1 = y as Element of COMPLEX by COMPLFLD:def 1;
thus f . y = x1 * ((id COMPLEX ) . y1) by VALUED_1:6
.= x * y by FUNCT_1:35
.= x * ((power F_Complex ) . y,1) by GROUP_1:98 ; :: thesis: verum

end;

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