theorem :: COMSEQ_3:11

for z being Complex holds z |^ 0 = 1r by COMPLEX1:def 4, NEWTON:4;