let s be Nat; :: thesis: for z being complex number holds z |^ (s + 1) = (z |^ s) * z
let z be complex number ; :: thesis: z |^ (s + 1) = (z |^ s) * z
defpred S₁[ Nat] means z |^ ($1 + 1) = (z |^ $1) * z;
reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
z |^ (s + 1) = Product ((s |-> z) ^ <*z*>) by FINSEQ_2:60
.= (Product (s |-> z)) * z by RVSUM_1:96 ;
hence z |^ (s + 1) = (z |^ s) * z ; :: thesis: verum