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:234;
defpred S₁[ Element of NAT ] means (z + w) |^ $1 = (Partial_Sums (Expan $1,z,w)) . $1;
A2: (Partial_Sums (Expan 0 ,z,w)) . 0 = (Expan 0 ,z,w) . 0 by COMSEQ_3:def 7
.= (((Coef 0 ) . 0 ) * (z |^ 0 )) * (w |^ 0 ) by A1, Def13
.= ((1 / (1 * 1)) * (z |^ 0 )) * (w |^ 0 ) by A1, Def10, Th1
.= 1r * ((w GeoSeq ) . 0 ) by COMSEQ_3:def 1
.= 1r by COMSEQ_3:def 1 ;
A3: S₁[ 0 ] by A2, COMSEQ_3:def 1;
A4: 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 A5: (z + w) |^ n = (Partial_Sums (Expan n,z,w)) . n ; :: thesis: S₁[n + 1]
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 A5, VALUED_1:6
.= (Partial_Sums ((z + w) (#) (Expan n,z,w))) . n by COMSEQ_3:29 ;

A7: now

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;

A8: (z + w) (#) (Expan n,z,w) = (z (#) (Expan n,z,w)) + (w (#) (Expan n,z,w)) by A7, FUNCT_2:113;
A9: (z + w) |^ (n + 1) = ((Partial_Sums (z (#) (Expan n,z,w))) + (Partial_Sums (w (#) (Expan n,z,w)))) . n by A6, A8, COMSEQ_3:27
.= ((Partial_Sums (z (#) (Expan n,z,w))) . n) + ((Partial_Sums (w (#) (Expan n,z,w))) . n) by VALUED_1:1 ;
A10: (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 COMSEQ_3:def 7
.= ((Partial_Sums (z (#) (Expan n,z,w))) . n) + (z * ((Expan n,z,w) . (n + 1))) by VALUED_1:6 ;
A11: n < n + 1 by XREAL_1:31;
A12: (Expan n,z,w) . (n + 1) = 0c by A11, Def13;
A13: (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 COMSEQ_3:def 7
.= ((Partial_Sums (w (#) (Expan n,z,w))) . n) + (w * ((Expan n,z,w) . (n + 1))) by VALUED_1:6 ;
A14: (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 Th6;
A15: 0 + n < n + 1 by XREAL_1:31;
A16: (Expan n,z,w) . (n + 1) = 0c by A15, Def13;
A17: z * ((Expan n,z,w) . (n + 1)) = 0c by A16;
A18: (Partial_Sums (z (#) (Expan n,z,w))) . (n + 1) = ((Partial_Sums (Shift (z (#) (Expan n,z,w)))) . (n + 1)) + 0c by A14, A17, VALUED_1:6
.= (Partial_Sums (Shift (z (#) (Expan n,z,w)))) . (n + 1) ;

A19: now

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

A20: now

assume A21: n + 1 < k ; :: thesis: ((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . k
A22: 0 + 1 <= n + 1 by XREAL_1:8;
A23: (n + 1) - 1 < k - 1 by A21, XREAL_1:11;
A24: n + 0 < (k - 1) + 1 by A23, XREAL_1:10;
A25: k - 1 = k -' 1 by A21, A22, XREAL_1:235, XXREAL_0:2;
A26: ((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 A24, Th5
.= (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 A24, Def13
.= 0c + (z * 0c ) by A23, A25, Def13
.= 0c ;
thus ((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . k by A21, A26, Def13; :: thesis: verum

end;

A27: now

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

A29: now

assume A30: k = n + 1 ; :: thesis: ((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . k
A31: n < n + 1 by XREAL_1:31;
A32: n -' n = n - n by XREAL_1:235
.= 0 ;
A33: (n + 1) -' (n + 1) = (n + 1) - (n + 1) by XREAL_1:235
.= 0 ;
A34: (Coef n) . n = (n !c ) / ((n !c ) * (0 !c )) by A32, Def10
.= 1 by Th1, XCMPLX_1:60 ;
A35: (Coef (n + 1)) . (n + 1) = ((n + 1) !c ) / (((n + 1) !c ) * (0 !c )) by A33, Def10
.= 1 by Th1, XCMPLX_1:60 ;
A36: ((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 A30, 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 A31, Def13
.= (z (#) (Expan n,z,w)) . n by Def12
.= z * ((Expan n,z,w) . n) by VALUED_1:6
.= z * ((((Coef n) . n) * (z |^ n)) * (w |^ (n -' n))) by Def13
.= (((Coef n) . n) * (((z GeoSeq ) . n) * z)) * (w |^ (n -' n))
.= (((Coef (n + 1)) . (n + 1)) * (z |^ (n + 1))) * (w |^ (n -' n)) by A34, A35, COMSEQ_3:def 1
.= (Expan (n + 1),z,w) . k by A30, A32, A33, Def13 ;
thus ((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . k by A36; :: thesis: verum

end;

A37: now

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

A39: now

assume A40: k = 0 ; :: thesis: ((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . k
A41: n -' 0 = n - 0 by XREAL_1:235;
A42: (n + 1) -' 0 = (n + 1) - 0 by XREAL_1:235;
A43: (Coef n) . 0 = (n !c ) / ((0 !c ) * (n !c )) by A41, Def10
.= 1 by Th1, XCMPLX_1:60 ;
A44: (Coef (n + 1)) . 0 = ((n + 1) !c ) / ((0 !c ) * ((n + 1) !c )) by A42, Def10
.= 1 by Th1, XCMPLX_1:60 ;
A45: ((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 A40, 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 Def12
.= w * ((((Coef n) . 0 ) * (z |^ 0 )) * (w |^ (n -' 0 ))) by Def13
.= (((Coef n) . 0 ) * (z |^ 0 )) * (((w GeoSeq ) . n) * w) by A41
.= (((Coef (n + 1)) . 0 ) * (z |^ 0 )) * (w |^ ((n + 1) -' 0 )) by A42, A43, A44, COMSEQ_3:def 1
.= (Expan (n + 1),z,w) . k by A40, Def13 ;
thus ((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . k by A45; :: thesis: verum

end;

A46: now

assume A47: k <> 0 ; :: thesis: ((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . k
A48: 0 + 1 <= k by A47, INT_1:20;
A49: (k + 1) - 1 <= (n + 1) - 1 by A38, INT_1:20;
A50: k < k + 1 by XREAL_1:31;
A51: k - 1 <= (k + 1) - 1 by A50, XREAL_1:11;
A52: k - 1 <= n by A49, A51, XXREAL_0:2;
A53: k -' 1 <= n by A48, A52, XREAL_1:235;
A54: ((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 A47, Th5
.= (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 A49, Def13
.= ((w * (((Coef n) . k) * (z |^ k))) * (w |^ (n -' k))) + (z * ((((Coef n) . (k -' 1)) * (z |^ (k -' 1))) * (w |^ (n -' (k -' 1))))) by A53, Def13
.= (((Coef n) . k) * ((w * (z |^ k)) * (w |^ (n -' k)))) + (((Coef n) . (k -' 1)) * (((z |^ (k -' 1)) * z) * (w |^ (n -' (k -' 1))))) ;
A55: (n -' k) + 1 = (n - k) + 1 by A49, XREAL_1:235
.= (n + 1) - k
.= (n + 1) -' k by A38, XREAL_1:235 ;
A56: n -' (k -' 1) = n - (k -' 1) by A53, XREAL_1:235
.= n - (k - 1) by A48, XREAL_1:235
.= (n + 1) - k
.= (n + 1) -' k by A38, XREAL_1:235 ;
A57: (k -' 1) + 1 = (k - 1) + 1 by A48, XREAL_1:235
.= k ;
A58: ( (w |^ (n -' k)) * w = w |^ ((n -' k) + 1) & (z |^ (k -' 1)) * z = z |^ k ) by A57, COMSEQ_3:def 1;
A59: ((Coef n) . k) + ((Coef n) . (k -' 1)) = ((n !c ) / ((k !c ) * ((n -' k) !c ))) + ((Coef n) . (k -' 1)) by A49, Def10
.= ((n !c ) / ((k !c ) * ((n -' k) !c ))) + ((n !c ) / (((k -' 1) !c ) * ((n -' (k -' 1)) !c ))) by A53, Def10 ;
A60: ((k !c ) * ((n -' k) !c )) * (((n + 1) - k) + (0 * <i> )) = (k !c ) * (((n -' k) !c ) * (((n + 1) - k) + (0 * <i> ))) ;
A61: (((k -' 1) !c ) * ((n -' (k -' 1)) !c )) * (k + (0 * <i> )) = ((k + (0 * <i> )) * ((k -' 1) !c )) * ((n -' (k -' 1)) !c )
.= (k !c ) * (((n + 1) -' k) !c ) by A47, A56, Th3 ;
A62: ((n + 1) - k) + (0 * <i> ) <> 0c by A38;
A63: (n !c ) / ((k !c ) * ((n -' k) !c )) = ((n !c ) * (((n + 1) - k) + (0 * <i> ))) / (((k !c ) * ((n -' k) !c )) * (((n + 1) - k) + (0 * <i> ))) by A62, XCMPLX_1:92
.= ((n !c ) * (((n + 1) - k) + (0 * <i> ))) / ((k !c ) * (((n + 1) -' k) !c )) by A49, A60, Th3 ;
A64: (n !c ) / (((k -' 1) !c ) * ((n -' (k -' 1)) !c )) = ((n !c ) * (k + (0 * <i> ))) / ((k !c ) * (((n + 1) -' k) !c )) by A47, A61, XCMPLX_1:92;
A65: ((Coef n) . k) + ((Coef n) . (k -' 1)) = ((n !c ) * ((((n + 1) - k) + k) + ((0 + 0 ) * <i> ))) / ((k !c ) * (((n + 1) -' k) !c )) by A59, A63, A64
.= ((n + 1) !c ) / ((k !c ) * (((n + 1) -' k) !c )) by Th1
.= (Coef (n + 1)) . k by A38, Def10 ;
A66: ((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (((Coef (n + 1)) . k) * (z |^ k)) * (w |^ ((n + 1) -' k)) by A54, A55, A56, A58, A65
.= (Expan (n + 1),z,w) . k by A38, Def13 ;
thus ((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . k by A66; :: thesis: verum

end;

thus ((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . k by A39, A46; :: thesis: verum

end;

thus ((w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w)))) . k = (Expan (n + 1),z,w) . k by A28, A29, A37, XXREAL_0:1; :: thesis: verum

end;

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

end;

A67: (w (#) (Expan n,z,w)) + (Shift (z (#) (Expan n,z,w))) = Expan (n + 1),z,w by A19, FUNCT_2:113;
thus (z + w) |^ (n + 1) = ((Partial_Sums (w (#) (Expan n,z,w))) + (Partial_Sums (Shift (z (#) (Expan n,z,w))))) . (n + 1) by A9, A10, A12, A13, A18, VALUED_1:1
.= (Partial_Sums (Expan (n + 1),z,w)) . (n + 1) by A67, COMSEQ_3:27 ; :: thesis: verum

end;

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