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