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