theorem Th3: :: BASEL_2:3

for n being Nat holds (1_ F_Complex) |^ n = 1_ F_Complex