let n be Nat; :: thesis: (1_ F_Complex) |^ n = 1_ F_Complex
thus (1_ F_Complex) |^ n = 1r |^ n by COMPLFLD:8, COMPLFLD:74
.= 1_ F_Complex by COMPLFLD:8, COMPLEX1:def 4 ; :: thesis: verum