let s be Nat; :: thesis: for z being Complex holds z |^ (s + 1) = (z |^ s) * z
let z be Complex; :: thesis: z |^ (s + 1) = (z |^ s) * z
thus z |^ (s + 1) = Product ((s |-> z) ^ <*z*>) by FINSEQ_2:60
.= (z |^ s) * z by RVSUM_1:96 ; :: thesis: verum