the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
then reconsider f = (id COMPLEX) (#) (id COMPLEX) as Function of F_Complex,F_Complex ;

now :: thesis: for x being Element of F_Complex holds f . x = (1_ F_Complex) * (power (x,2))

let x be Element of F_Complex; :: thesis: f . x = (1_ F_Complex) * (power (x,2))
reconsider x1 = x as Element of COMPLEX by COMPLFLD:def 1;
( (id COMPLEX) /. x1 = x1 & dom ((id COMPLEX) (#) (id COMPLEX)) = COMPLEX ) by FUNCT_2:def 1;
hence f . x = x * x by VALUED_1:def 4
.= (power F_Complex) . (x,2) by GROUP_1:51
.= (1_ F_Complex) * (power (x,2)) ;
:: thesis: verum

end;

hence FPower ((1_ F_Complex),2) = (id COMPLEX) (#) (id COMPLEX) by Def12; :: thesis: verum