let z be complex number ; :: thesis: z |^ 1 = z
reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
z |^ 1 = Product <*z*> by FINSEQ_2:59
.= z by RVSUM_1:95 ;
hence z |^ 1 = z ; :: thesis: verum