let z, w be Element of COMPLEX ; :: thesis: for n being Element of NAT holds (z + w) |^ n = (Partial_Sums (Expan (n,z,w))) . n
let n be Element of NAT ; :: thesis: (z + w) |^ n = (Partial_Sums (Expan (n,z,w))) . n
A1: 0 -' 0 = 0 by XREAL_1:232;
defpred S₁[ Element of NAT ] means (z + w) |^ $1 = (Partial_Sums (Expan ($1,z,w))) . $1;
(Partial_Sums (Expan (0,z,w))) . 0 = (Expan (0,z,w)) . 0 by SERIES_1:def 1
.= (((Coef 0) . 0) * (z |^ 0)) * (w |^ 0) by A1, Def9
.= ((1 / (1 * 1)) * (z |^ 0)) * (w |^ 0) by A1, Def6, Th1
.= 1r * ((w GeoSeq) . 0) by COMSEQ_3:def 1
.= 1r by COMSEQ_3:def 1 ;
then A2: S₁[ 0 ] by COMSEQ_3:def 1;
A3: 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 A4: (z + w) |^ n = (Partial_Sums (Expan (n,z,w))) . n ; :: thesis: S₁[n + 1]
A5: (z + w) |^ (n + 1) = (((z + w) GeoSeq) . n) * (z + w) by COMSEQ_3:def 1
.= ((z + w) (#) (Partial_Sums (Expan (n,z,w)))) . n by A4, VALUED_1:6
.= (Partial_Sums ((z + w) (#) (Expan (n,z,w)))) . n by COMSEQ_3:29 ;

now :: thesis: for k being Element of NAT holds ((z + w) (#) (Expan (n,z,w))) . k = ((z (#) (Expan (n,z,w))) + (w (#) (Expan (n,z,w)))) . k

let k be Element of NAT ; :: thesis: ((z + w) (#) (Expan (n,z,w))) . k = ((z (#) (Expan (n,z,w))) + (w (#) (Expan (n,z,w)))) . k
thus ((z + w) (#) (Expan (n,z,w))) . k = (z + w) * ((Expan (n,z,w)) . k) by VALUED_1:6
.= (z * ((Expan (n,z,w)) . k)) + (w * ((Expan (n,z,w)) . k))
.= ((z (#) (Expan (n,z,w))) . k) + (w * ((Expan (n,z,w)) . k)) by VALUED_1:6
.= ((z (#) (Expan (n,z,w))) . k) + ((w (#) (Expan (n,z,w))) . k) by VALUED_1:6
.= ((z (#) (Expan (n,z,w))) + (w (#) (Expan (n,z,w)))) . k by VALUED_1:1 ; :: thesis: verum

end;

then (z + w) (#) (Expan (n,z,w)) = (z (#) (Expan (n,z,w))) + (w (#) (Expan (n,z,w))) by FUNCT_2:63;
then A6: (z + w) |^ (n + 1) = ((Partial_Sums (z (#) (Expan (n,z,w)))) + (Partial_Sums (w (#) (Expan (n,z,w))))) . n by A5, COMSEQ_3:27
.= ((Partial_Sums (z (#) (Expan (n,z,w)))) . n) + ((Partial_Sums (w (#) (Expan (n,z,w)))) . n) by VALUED_1:1 ;
A7: (Partial_Sums (z (#) (Expan (n,z,w)))) . (n + 1) = ((Partial_Sums (z (#) (Expan (n,z,w)))) . n) + ((z (#) (Expan (n,z,w))) . (n + 1)) by SERIES_1:def 1
.= ((Partial_Sums (z (#) (Expan (n,z,w)))) . n) + (z * ((Expan (n,z,w)) . (n + 1))) by VALUED_1:6 ;
n < n + 1 by XREAL_1:29;
then A8: (Expan (n,z,w)) . (n + 1) = 0c by Def9;
A9: (Partial_Sums (w (#) (Expan (n,z,w)))) . (n + 1) = ((Partial_Sums (w (#) (Expan (n,z,w)))) . n) + ((w (#) (Expan (n,z,w))) . (n + 1)) by SERIES_1:def 1
.= ((Partial_Sums (w (#) (Expan (n,z,w)))) . n) + (w * ((Expan (n,z,w)) . (n + 1))) by VALUED_1:6 ;
A10: (Partial_Sums (z (#) (Expan (n,z,w)))) . (n + 1) = ((Partial_Sums (Shift (z (#) (Expan (n,z,w))))) . (n + 1)) + ((z (#) (Expan (n,z,w))) . (n + 1)) by Th5;
0 + n < n + 1 by XREAL_1:29;
then (Expan (n,z,w)) . (n + 1) = 0c by Def9;
then z * ((Expan (n,z,w)) . (n + 1)) = 0c ;
then A11: (Partial_Sums (z (#) (Expan (n,z,w)))) . (n + 1) = ((Partial_Sums (Shift (z (#) (Expan (n,z,w))))) . (n + 1)) + 0c by A10, VALUED_1:6
.= (Partial_Sums (Shift (z (#) (Expan (n,z,w))))) . (n + 1) ;

now :: thesis: for k being Element of NAT holds ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k

let k be Element of NAT ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k

A12: now :: thesis: ( n + 1 < k implies ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k )

assume A13: n + 1 < k ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k
A14: 0 + 1 <= n + 1 by XREAL_1:6;
A15: (n + 1) - 1 < k - 1 by A13, XREAL_1:9;
then A16: n + 0 < (k - 1) + 1 by XREAL_1:8;
A17: k - 1 = k -' 1 by A13, A14, XREAL_1:233, XXREAL_0:2;
((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = ((w (#) (Expan (n,z,w))) . k) + ((Shift (z (#) (Expan (n,z,w)))) . k) by VALUED_1:1
.= (w * ((Expan (n,z,w)) . k)) + ((Shift (z (#) (Expan (n,z,w)))) . k) by VALUED_1:6
.= (w * ((Expan (n,z,w)) . k)) + ((z (#) (Expan (n,z,w))) . (k -' 1)) by A16, Th4
.= (w * ((Expan (n,z,w)) . k)) + (z * ((Expan (n,z,w)) . (k -' 1))) by VALUED_1:6
.= (w * 0c) + (z * ((Expan (n,z,w)) . (k -' 1))) by A16, Def9
.= 0c + (z * 0c) by A15, A17, Def9
.= 0c ;
hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k by A13, Def9; :: thesis: verum

end;

now :: thesis: ( k <= n + 1 implies ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k )

assume A18: k <= n + 1 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k

A19: now :: thesis: ( k = n + 1 implies ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k )

assume A20: k = n + 1 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k
A21: n < n + 1 by XREAL_1:29;
A22: n -' n = n - n by XREAL_1:233
.= 0 ;
A23: (n + 1) -' (n + 1) = (n + 1) - (n + 1) by XREAL_1:233
.= 0 ;
A24: (Coef n) . n = (n !) / ((n !) * (0 !)) by A22, Def6
.= 1 by Th1, XCMPLX_1:60 ;
A25: (Coef (n + 1)) . (n + 1) = ((n + 1) !) / (((n + 1) !) * (0 !)) by A23, Def6
.= 1 by Th1, XCMPLX_1:60 ;
((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = ((w (#) (Expan (n,z,w))) . (n + 1)) + ((Shift (z (#) (Expan (n,z,w)))) . (n + 1)) by A20, VALUED_1:1
.= (w * ((Expan (n,z,w)) . (n + 1))) + ((Shift (z (#) (Expan (n,z,w)))) . (n + 1)) by VALUED_1:6
.= (w * 0c) + ((Shift (z (#) (Expan (n,z,w)))) . (n + 1)) by A21, Def9
.= (z (#) (Expan (n,z,w))) . n by Def8
.= z * ((Expan (n,z,w)) . n) by VALUED_1:6
.= z * ((((Coef n) . n) * (z |^ n)) * (w |^ (n -' n))) by Def9
.= (((Coef n) . n) * (((z GeoSeq) . n) * z)) * (w |^ (n -' n))
.= (((Coef (n + 1)) . (n + 1)) * (z |^ (n + 1))) * (w |^ (n -' n)) by A24, A25, COMSEQ_3:def 1
.= (Expan ((n + 1),z,w)) . k by A20, A22, A23, Def9 ;
hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k ; :: thesis: verum

end;

now :: thesis: ( k < n + 1 implies ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k )

assume A26: k < n + 1 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k

A27: now :: thesis: ( k = 0 implies ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k )

assume A28: k = 0 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k
A29: n -' 0 = n - 0 by XREAL_1:233;
A30: (n + 1) -' 0 = (n + 1) - 0 by XREAL_1:233;
A31: (Coef n) . 0 = (n !) / ((0 !) * (n !)) by A29, Def6
.= 1 by Th1, XCMPLX_1:60 ;
A32: (Coef (n + 1)) . 0 = ((n + 1) !) / ((0 !) * ((n + 1) !)) by A30, Def6
.= 1 by Th1, XCMPLX_1:60 ;
((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = ((w (#) (Expan (n,z,w))) . 0) + ((Shift (z (#) (Expan (n,z,w)))) . 0) by A28, VALUED_1:1
.= (w * ((Expan (n,z,w)) . 0)) + ((Shift (z (#) (Expan (n,z,w)))) . 0) by VALUED_1:6
.= (w * ((Expan (n,z,w)) . 0)) + 0c by Def8
.= w * ((((Coef n) . 0) * (z |^ 0)) * (w |^ (n -' 0))) by Def9
.= (((Coef n) . 0) * (z |^ 0)) * (((w GeoSeq) . n) * w) by A29
.= (((Coef (n + 1)) . 0) * (z |^ 0)) * (w |^ ((n + 1) -' 0)) by A30, A31, A32, COMSEQ_3:def 1
.= (Expan ((n + 1),z,w)) . k by A28, Def9 ;
hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k ; :: thesis: verum

end;

now :: thesis: ( k <> 0 implies ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k )

assume A33: k <> 0 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k
then A34: 0 + 1 <= k by INT_1:7;
A35: (k + 1) - 1 <= (n + 1) - 1 by A26, INT_1:7;
k < k + 1 by XREAL_1:29;
then k - 1 <= (k + 1) - 1 by XREAL_1:9;
then k - 1 <= n by A35, XXREAL_0:2;
then A36: k -' 1 <= n by A34, XREAL_1:233;
A37: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = ((w (#) (Expan (n,z,w))) . k) + ((Shift (z (#) (Expan (n,z,w)))) . k) by VALUED_1:1
.= (w * ((Expan (n,z,w)) . k)) + ((Shift (z (#) (Expan (n,z,w)))) . k) by VALUED_1:6
.= (w * ((Expan (n,z,w)) . k)) + ((z (#) (Expan (n,z,w))) . (k -' 1)) by A33, Th4
.= (w * ((Expan (n,z,w)) . k)) + (z * ((Expan (n,z,w)) . (k -' 1))) by VALUED_1:6
.= (w * ((((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)))) + (z * ((Expan (n,z,w)) . (k -' 1))) by A35, Def9
.= ((w * (((Coef n) . k) * (z |^ k))) * (w |^ (n -' k))) + (z * ((((Coef n) . (k -' 1)) * (z |^ (k -' 1))) * (w |^ (n -' (k -' 1))))) by A36, Def9
.= (((Coef n) . k) * ((w * (z |^ k)) * (w |^ (n -' k)))) + (((Coef n) . (k -' 1)) * (((z |^ (k -' 1)) * z) * (w |^ (n -' (k -' 1))))) ;
A38: (n -' k) + 1 = (n - k) + 1 by A35, XREAL_1:233
.= (n + 1) - k
.= (n + 1) -' k by A26, XREAL_1:233 ;
A39: n -' (k -' 1) = n - (k -' 1) by A36, XREAL_1:233
.= n - (k - 1) by A34, XREAL_1:233
.= (n + 1) - k
.= (n + 1) -' k by A26, XREAL_1:233 ;
(k -' 1) + 1 = (k - 1) + 1 by A34, XREAL_1:233
.= k ;
then A40: ( (w |^ (n -' k)) * w = w |^ ((n -' k) + 1) & (z |^ (k -' 1)) * z = z |^ k ) by COMSEQ_3:def 1;
A41: ((Coef n) . k) + ((Coef n) . (k -' 1)) = ((n !) / ((k !) * ((n -' k) !))) + ((Coef n) . (k -' 1)) by A35, Def6
.= ((n !) / ((k !) * ((n -' k) !))) + ((n !) / (((k -' 1) !) * ((n -' (k -' 1)) !))) by A36, Def6 ;
A42: ((k !) * ((n -' k) !)) * (((n + 1) - k) + (0 * <i>)) = (k !) * (((n -' k) !) * (((n + 1) - k) + (0 * <i>))) ;
A43: (((k -' 1) !) * ((n -' (k -' 1)) !)) * (k + (0 * <i>)) = ((k + (0 * <i>)) * ((k -' 1) !)) * ((n -' (k -' 1)) !)
.= (k !) * (((n + 1) -' k) !) by A33, A39, Th2 ;
((n + 1) - k) + (0 * <i>) <> 0c by A26;
then A44: (n !) / ((k !) * ((n -' k) !)) = ((n !) * (((n + 1) - k) + (0 * <i>))) / (((k !) * ((n -' k) !)) * (((n + 1) - k) + (0 * <i>))) by XCMPLX_1:91
.= ((n !) * (((n + 1) - k) + (0 * <i>))) / ((k !) * (((n + 1) -' k) !)) by A35, A42, Th2 ;
(n !) / (((k -' 1) !) * ((n -' (k -' 1)) !)) = ((n !) * (k + (0 * <i>))) / ((k !) * (((n + 1) -' k) !)) by A33, A43, XCMPLX_1:91;
then ((Coef n) . k) + ((Coef n) . (k -' 1)) = ((n !) * ((((n + 1) - k) + k) + ((0 + 0) * <i>))) / ((k !) * (((n + 1) -' k) !)) by A41, A44
.= ((n + 1) !) / ((k !) * (((n + 1) -' k) !)) by Th1
.= (Coef (n + 1)) . k by A26, Def6 ;
then ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (((Coef (n + 1)) . k) * (z |^ k)) * (w |^ ((n + 1) -' k)) by A37, A38, A39, A40
.= (Expan ((n + 1),z,w)) . k by A26, Def9 ;
hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k ; :: thesis: verum

end;

hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k by A27; :: thesis: verum

end;

hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k by A18, A19, XXREAL_0:1; :: thesis: verum

end;

hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k by A12; :: thesis: verum

end;

then A45: (w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w)))) = Expan ((n + 1),z,w) by FUNCT_2:63;
thus (z + w) |^ (n + 1) = ((Partial_Sums (w (#) (Expan (n,z,w)))) + (Partial_Sums (Shift (z (#) (Expan (n,z,w)))))) . (n + 1) by A6, A7, A8, A9, A11, VALUED_1:1
.= (Partial_Sums (Expan ((n + 1),z,w))) . (n + 1) by A45, COMSEQ_3:27 ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
hence (z + w) |^ n = (Partial_Sums (Expan (n,z,w))) . n ; :: thesis: verum