let z be Complex; :: thesis: z |^ 1 = z
thus z |^ 1 = Product <*z*> by FINSEQ_2:59
.= z by RVSUM_1:95 ; :: thesis: verum