defpred S₁[ Nat] means for z being Complex holds ((cos_C /. z) + (<i> * (sin_C /. z))) |^ $1 = (cos_C /. ($1 * z)) + (<i> * (sin_C /. ($1 * z)));
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: for z being Complex holds ((cos_C /. z) + (<i> * (sin_C /. z))) |^ n = (cos_C /. (n * z)) + (<i> * (sin_C /. (n * z))) ; :: thesis: S₁[n + 1]
for z being Complex holds ((cos_C /. z) + (<i> * (sin_C /. z))) |^ (n + 1) = (cos_C /. ((n + 1) * z)) + (<i> * (sin_C /. ((n + 1) * z)))

proof

let z be Complex; :: thesis: ((cos_C /. z) + (<i> * (sin_C /. z))) |^ (n + 1) = (cos_C /. ((n + 1) * z)) + (<i> * (sin_C /. ((n + 1) * z)))
set cn = cos_C /. (n * z);
set sn = sin_C /. (n * z);
set c1 = cos_C /. z;
set s1 = sin_C /. z;
A3: ((cos_C /. z) + (<i> * (sin_C /. z))) |^ (n + 1) = (((cos_C /. z) + (<i> * (sin_C /. z))) GeoSeq) . (n + 1) by COMSEQ_3:def 2
.= ((((cos_C /. z) + (<i> * (sin_C /. z))) GeoSeq) . n) * ((cos_C /. z) + (<i> * (sin_C /. z))) by COMSEQ_3:def 1
.= (((cos_C /. z) + (<i> * (sin_C /. z))) |^ n) * ((cos_C /. z) + (<i> * (sin_C /. z))) by COMSEQ_3:def 2
.= ((cos_C /. (n * z)) + (<i> * (sin_C /. (n * z)))) * ((cos_C /. z) + (<i> * (sin_C /. z))) by A2
.= (((cos_C /. (n * z)) * (cos_C /. z)) + ((<i> * (sin_C /. (n * z))) * (cos_C /. z))) + (((<i> * (cos_C /. (n * z))) * (sin_C /. z)) + (- ((sin_C /. (n * z)) * (sin_C /. z)))) ;
(cos_C /. ((n + 1) * z)) + (<i> * (sin_C /. ((n + 1) * z))) = (cos_C /. ((n * z) + (1 * z))) + (<i> * (((sin_C /. (n * z)) * (cos_C /. (1 * z))) + ((cos_C /. (n * z)) * (sin_C /. (1 * z))))) by Th4
.= (((cos_C /. (n * z)) * (cos_C /. z)) - ((sin_C /. (n * z)) * (sin_C /. z))) + (<i> * (((sin_C /. (n * z)) * (cos_C /. z)) + ((cos_C /. (n * z)) * (sin_C /. z)))) by Th6
.= ((cos_C /. (n * z)) * (cos_C /. z)) + (((<i> * (sin_C /. (n * z))) * (cos_C /. z)) + (((<i> * (cos_C /. (n * z))) * (sin_C /. z)) + (- ((sin_C /. (n * z)) * (sin_C /. z))))) ;
hence ((cos_C /. z) + (<i> * (sin_C /. z))) |^ (n + 1) = (cos_C /. ((n + 1) * z)) + (<i> * (sin_C /. ((n + 1) * z))) by A3; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A4: S₁[ 0 ] by Th21, Th23, COMPLEX1:def 4, COMSEQ_3:11;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A1);
hence for n being Element of NAT
for z being Complex holds ((cos_C /. z) + (<i> * (sin_C /. z))) |^ n = (cos_C /. (n * z)) + (<i> * (sin_C /. (n * z))) ; :: thesis: verum