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 :: thesis: for y being Element of F_Complex holds f . y = x * (power (y,1))
let y be Element of F_Complex; :: thesis: f . y = x * (power (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
.= x * (power (y,1)) by GROUP_1:50 ; :: thesis: verum
end;
hence FPower (x,1) = x1 (#) (id COMPLEX) by Def12; :: thesis: verum