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;
A1: S₁[ 0 ]

proof

reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
z |^ (0 + 1) = Product <*z*> by FINSEQ_2:73
.= 1 * z by RVSUM_1:125 ;
hence S₁[ 0 ] by RVSUM_1:124; :: thesis: verum

end;

A2: for s being Nat st S₁[s] holds
S₁[s + 1]

proof

let s be Nat; :: thesis: ( S₁[s] implies S₁[s + 1] )
assume z |^ (s + 1) = (z |^ s) * z ; :: thesis: S₁[s + 1]
reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
z |^ ((s + 1) + 1) = Product (((s + 1) |-> z) ^ <*z*>) by FINSEQ_2:74
.= (Product ((s + 1) |-> z)) * z by RVSUM_1:126 ;
hence S₁[s + 1] ; :: thesis: verum

end;

for s being Nat holds S₁[s] from NAT_1:sch 2(A1, A2);
hence z |^ (s + 1) = (z |^ s) * z ; :: thesis: verum