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

let x be Element of F_Complex ; :: thesis: f . x = (1_ F_Complex ) * ((power F_Complex ) . 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_1:35, FUNCT_2:def 1;
hence f . x = x * x by VALUED_1:def 4
.= (power F_Complex ) . x,2 by GROUP_1:99
.= (1_ F_Complex ) * ((power F_Complex ) . x,2) by VECTSP_1:def 19 ;
:: thesis: verum

end;

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