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