let w, z be Complex; :: thesis: for n being Nat holds (z + w) |^ n = (Partial_Sums (Expan (n,z,w))) . n
let n be Nat; :: thesis: (z + w) |^ n = (Partial_Sums (Expan (n,z,w))) . n
A1: 0 -' 0 = 0 by XREAL_1:232;
defpred S₁[ 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 Nat st S₁[n] holds
S₁[n + 1]

proof

let n be 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: n in NAT by ORDINAL1:def 12;
A6: (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))) ;
then A7: (z + w) |^ (n + 1) = ((Partial_Sums (z (#) (Expan (n,z,w)))) + (Partial_Sums (w (#) (Expan (n,z,w))))) . n by A6, COMSEQ_3:27
.= ((Partial_Sums (z (#) (Expan (n,z,w)))) . n) + ((Partial_Sums (w (#) (Expan (n,z,w)))) . n) by VALUED_1:1, A5 ;
A8: (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 A9: (Expan (n,z,w)) . (n + 1) = 0c by Def9;
A10: (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 ;
A11: (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 A12: (Partial_Sums (z (#) (Expan (n,z,w)))) . (n + 1) = ((Partial_Sums (Shift (z (#) (Expan (n,z,w))))) . (n + 1)) + 0c by A11, 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

A13: 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 A14: n + 1 < k ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k
A15: 0 + 1 <= n + 1 by XREAL_1:6;
A16: (n + 1) - 1 < k - 1 by A14, XREAL_1:9;
then A17: n + 0 < (k - 1) + 1 by XREAL_1:8;
A18: k - 1 = k -' 1 by A14, A15, 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 A17, 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 A17, Def9
.= 0c + (z * 0c) by A16, A18, Def9
.= 0c ;
hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k by A14, 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 A19: k <= n + 1 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k

A20: 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 A21: k = n + 1 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k
A22: n < n + 1 by XREAL_1:29;
A23: n -' n = n - n by XREAL_1:233
.= 0 ;
A24: (n + 1) -' (n + 1) = (n + 1) - (n + 1) by XREAL_1:233
.= 0 ;
A25: (Coef n) . n = (n !) / ((n !) * (0 !)) by A23, Def6
.= 1 by Th1, XCMPLX_1:60 ;
A26: (Coef (n + 1)) . (n + 1) = ((n + 1) !) / (((n + 1) !) * (0 !)) by A24, 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 A21, 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 A22, 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 A25, A26, COMSEQ_3:def 1
.= (Expan ((n + 1),z,w)) . k by A21, A23, A24, 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 A27: k < n + 1 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k

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

assume A29: k = 0 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k
A30: n -' 0 = n - 0 by XREAL_1:233;
A31: (n + 1) -' 0 = (n + 1) - 0 by XREAL_1:233;
A32: (Coef n) . 0 = (n !) / ((0 !) * (n !)) by A30, Def6
.= 1 by Th1, XCMPLX_1:60 ;
A33: (Coef (n + 1)) . 0 = ((n + 1) !) / ((0 !) * ((n + 1) !)) by A31, 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 A29, 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 A30
.= (((Coef (n + 1)) . 0) * (z |^ 0)) * (w |^ ((n + 1) -' 0)) by A31, A32, A33, COMSEQ_3:def 1
.= (Expan ((n + 1),z,w)) . k by A29, 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 A34: k <> 0 ; :: thesis: ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k
then A35: 0 + 1 <= k by INT_1:7;
A36: (k + 1) - 1 <= (n + 1) - 1 by A27, 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 A36, XXREAL_0:2;
then A37: k -' 1 <= n by A35, XREAL_1:233;
A38: ((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 A34, 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 A36, Def9
.= ((w * (((Coef n) . k) * (z |^ k))) * (w |^ (n -' k))) + (z * ((((Coef n) . (k -' 1)) * (z |^ (k -' 1))) * (w |^ (n -' (k -' 1))))) by A37, Def9
.= (((Coef n) . k) * ((w * (z |^ k)) * (w |^ (n -' k)))) + (((Coef n) . (k -' 1)) * (((z |^ (k -' 1)) * z) * (w |^ (n -' (k -' 1))))) ;
A39: (n -' k) + 1 = (n - k) + 1 by A36, XREAL_1:233
.= (n + 1) - k
.= (n + 1) -' k by A27, XREAL_1:233 ;
A40: n -' (k -' 1) = n - (k -' 1) by A37, XREAL_1:233
.= n - (k - 1) by A35, XREAL_1:233
.= (n + 1) - k
.= (n + 1) -' k by A27, XREAL_1:233 ;
(k -' 1) + 1 = (k - 1) + 1 by A35, XREAL_1:233
.= k ;
then A41: ( (w |^ (n -' k)) * w = w |^ ((n -' k) + 1) & (z |^ (k -' 1)) * z = z |^ k ) by COMSEQ_3:def 1;
A42: ((Coef n) . k) + ((Coef n) . (k -' 1)) = ((n !) / ((k !) * ((n -' k) !))) + ((Coef n) . (k -' 1)) by A36, Def6
.= ((n !) / ((k !) * ((n -' k) !))) + ((n !) / (((k -' 1) !) * ((n -' (k -' 1)) !))) by A37, Def6 ;
A43: ((k !) * ((n -' k) !)) * (((n + 1) - k) + (0 * <i>)) = (k !) * (((n -' k) !) * (((n + 1) - k) + (0 * <i>))) ;
A44: (((k -' 1) !) * ((n -' (k -' 1)) !)) * (k + (0 * <i>)) = ((k + (0 * <i>)) * ((k -' 1) !)) * ((n -' (k -' 1)) !)
.= (k !) * (((n + 1) -' k) !) by A34, A40, Th2 ;
((n + 1) - k) + (0 * <i>) <> 0c by A27;
then A45: (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 A36, A43, Th2 ;
(n !) / (((k -' 1) !) * ((n -' (k -' 1)) !)) = ((n !) * (k + (0 * <i>))) / ((k !) * (((n + 1) -' k) !)) by A34, A44, XCMPLX_1:91;
then ((Coef n) . k) + ((Coef n) . (k -' 1)) = ((n !) * ((((n + 1) - k) + k) + ((0 + 0) * <i>))) / ((k !) * (((n + 1) -' k) !)) by A42, A45
.= ((n + 1) !) / ((k !) * (((n + 1) -' k) !)) by Th1
.= (Coef (n + 1)) . k by A27, 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 A38, A39, A40, A41
.= (Expan ((n + 1),z,w)) . k by A27, 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 A28; :: thesis: verum

end;

hence ((w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w))))) . k = (Expan ((n + 1),z,w)) . k by A19, A20, 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 A13; :: thesis: verum

end;

then A46: (w (#) (Expan (n,z,w))) + (Shift (z (#) (Expan (n,z,w)))) = Expan ((n + 1),z,w) ;
thus (z + w) |^ (n + 1) = ((Partial_Sums (w (#) (Expan (n,z,w)))) + (Partial_Sums (Shift (z (#) (Expan (n,z,w)))))) . (n + 1) by A7, A8, A9, A10, A12, VALUED_1:1
.= (Partial_Sums (Expan ((n + 1),z,w))) . (n + 1) by A46, COMSEQ_3:27 ; :: thesis: verum

end;

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