let n be Element of NAT ; :: thesis: 1_ F_Complex = (power F_Complex) . ((1_ F_Complex),n)
1_ F_Complex = [**1,0**] by COMPLFLD:8;
then (power F_Complex) . ((1_ F_Complex),n) = [**(1 to_power n),0**] by HAHNBAN1:29
.= 1_ F_Complex by COMPLFLD:8 ;
hence 1_ F_Complex = (power F_Complex) . ((1_ F_Complex),n) ; :: thesis: verum