defpred S₁[ Element of NAT ] means for z being Element of COMPLEX holds ((cos_C /. z) + (<i> * (sin_C /. z))) #N $1 = (cos_C /. ($1 * z)) + (<i> * (sin_C /. ($1 * z)));
A1: S₁[ 0 ] by Th21, Th23, COMPLEX1:def 7, COMSEQ_3:11;
A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: for z being Element of COMPLEX holds ((cos_C /. z) + (<i> * (sin_C /. z))) #N n = (cos_C /. (n * z)) + (<i> * (sin_C /. (n * z))) ; :: thesis: S₁[n + 1]
for z being Element of COMPLEX holds ((cos_C /. z) + (<i> * (sin_C /. z))) #N (n + 1) = (cos_C /. ((n + 1) * z)) + (<i> * (sin_C /. ((n + 1) * z)))

proof

let z be Element of COMPLEX ; :: thesis: ((cos_C /. z) + (<i> * (sin_C /. z))) #N (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;
A5: ((cos_C /. z) + (<i> * (sin_C /. z))) #N (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 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 A3
.= (((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 (n + 1) = (cos_C /. ((n + 1) * z)) + (<i> * (sin_C /. ((n + 1) * z))) by A5; :: thesis: verum

end;

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

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence for n being Element of NAT
for z being Element of COMPLEX holds ((cos_C /. z) + (<i> * (sin_C /. z))) #N n = (cos_C /. (n * z)) + (<i> * (sin_C /. (n * z))) ; :: thesis: verum