let X be Banach_Algebra; :: thesis: for n being Nat
for z, w being Element of X st z,w are_commutative holds
(z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n
let n be Nat; :: thesis: for z, w being Element of X st z,w are_commutative holds
(z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n
let z, w be Element of X; :: thesis: ( z,w are_commutative implies (z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n )
assume A1: z,w are_commutative ; :: thesis: (z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n
defpred S₁[ Nat] means (z + w) #N $1 = (Partial_Sums (Expan ($1,z,w))) . $1;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: (z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n ; :: thesis: S₁[n + 1]
A4: n < n + 1 by XREAL_1:29;
A5: n in NAT by ORDINAL1:def 12;

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

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

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

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

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

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

A10: ((k !) * ((n -' k) !)) * ((n + 1) - k) = (k !) * (((n -' k) !) * ((n + 1) - k)) ;
A11: (k + 1) - 1 <= (n + 1) - 1 by A8, INT_1:7, A5;
then A12: (n -' k) + 1 = (n - k) + 1 by XREAL_1:233
.= (n + 1) - k
.= (n + 1) -' k by A8, XREAL_1:233 ;
(n + 1) - k <> 0 by A8;
then A13: (n !) / ((k !) * ((n -' k) !)) = ((n !) * ((n + 1) - k)) / (((k !) * ((n -' k) !)) * ((n + 1) - k)) by XCMPLX_1:91
.= ((n !) * ((n + 1) - k)) / ((k !) * (((n + 1) -' k) !)) by A11, A10, Th13 ;
assume A14: k <> 0 ; :: thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
then A15: 0 + 1 <= k by INT_1:7;
then A16: (k -' 1) + 1 = (k - 1) + 1 by XREAL_1:233
.= k ;
k < k + 1 by XREAL_1:29;
then k - 1 <= (k + 1) - 1 by XREAL_1:9;
then k - 1 <= n by A11, XXREAL_0:2;
then A17: k -' 1 <= n by A15, XREAL_1:233;
then A18: n -' (k -' 1) = n - (k -' 1) by XREAL_1:233
.= n - (k - 1) by A15, XREAL_1:233
.= (n + 1) - k
.= (n + 1) -' k by A8, XREAL_1:233 ;
A19: n -' (k -' 1) = n - (k -' 1) by A17, XREAL_1:233
.= n - (k - 1) by A15, XREAL_1:233
.= (n + 1) - k
.= (n + 1) -' k by A8, XREAL_1:233 ;
(((k -' 1) !) * ((n -' (k -' 1)) !)) * k = (k * ((k -' 1) !)) * ((n -' (k -' 1)) !)
.= (k !) * (((n + 1) -' k) !) by A14, A19, Th13 ;
then A20: (n !) / (((k -' 1) !) * ((n -' (k -' 1)) !)) = ((n !) * k) / ((k !) * (((n + 1) -' k) !)) by A14, XCMPLX_1:91;
(((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (((Expan (n,z,w)) * w) . k) + ((Shift ((Expan (n,z,w)) * z)) . k) by NORMSP_1:def 2
.= (((Expan (n,z,w)) . k) * w) + ((Shift ((Expan (n,z,w)) * z)) . k) by LOPBAN_3:def 6
.= (((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) * z) . (k -' 1)) by A14, Th15
.= (((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) . (k -' 1)) * z) by LOPBAN_3:def 6
.= (((((Coef n) . k) * (z #N k)) * (w #N (n -' k))) * w) + (((Expan (n,z,w)) . (k -' 1)) * z) by A11, Def6
.= (((((Coef n) . k) * (z #N k)) * (w #N (n -' k))) * w) + (((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * (w #N (n -' (k -' 1)))) * z) by A17, Def6
.= ((((Coef n) . k) * (z #N k)) * ((w #N (n -' k)) * w)) + (((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * (w #N (n -' (k -' 1)))) * z) by LOPBAN_3:38
.= ((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + (((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * (w #N (n -' (k -' 1)))) * z) by Lm1
.= ((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + ((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * ((w #N (n -' (k -' 1))) * z)) by LOPBAN_3:38
.= ((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + ((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * (z * (w #N (n -' (k -' 1))))) by A1, Lm2
.= ((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + (((((Coef n) . (k -' 1)) * (z #N (k -' 1))) * z) * (w #N (n -' (k -' 1)))) by LOPBAN_3:38
.= ((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + ((((Coef n) . (k -' 1)) * ((z #N (k -' 1)) * z)) * (w #N (n -' (k -' 1)))) by LOPBAN_3:38
.= ((((Coef n) . k) * (z #N k)) * (w #N ((n -' k) + 1))) + ((((Coef n) . (k -' 1)) * (z #N ((k -' 1) + 1))) * (w #N (n -' (k -' 1)))) by Lm1 ;
then A21: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (((Coef n) . k) * ((z #N k) * (w #N ((n + 1) -' k)))) + ((((Coef n) . (k -' 1)) * (z #N k)) * (w #N ((n + 1) -' k))) by A12, A18, A16, LOPBAN_3:38
.= (((Coef n) . k) * ((z #N k) * (w #N ((n + 1) -' k)))) + (((Coef n) . (k -' 1)) * ((z #N k) * (w #N ((n + 1) -' k)))) by LOPBAN_3:38
.= (((Coef n) . k) + ((Coef n) . (k -' 1))) * ((z #N k) * (w #N ((n + 1) -' k))) by LOPBAN_3:38 ;
((Coef n) . k) + ((Coef n) . (k -' 1)) = ((n !) / ((k !) * ((n -' k) !))) + ((Coef n) . (k -' 1)) by A11, Def3
.= ((n !) / ((k !) * ((n -' k) !))) + ((n !) / (((k -' 1) !) * ((n -' (k -' 1)) !))) by A17, Def3 ;
then ((Coef n) . k) + ((Coef n) . (k -' 1)) = (((n !) * ((n + 1) - k)) + ((n !) * k)) / ((k !) * (((n + 1) -' k) !)) by A13, A20, XCMPLX_1:62
.= ((n !) * (((n + 1) - k) + k)) / ((k !) * (((n + 1) -' k) !))
.= ((n + 1) !) / ((k !) * (((n + 1) -' k) !)) by NEWTON:15
.= (Coef (n + 1)) . k by A8, Def3 ;
then (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (((Coef (n + 1)) . k) * (z #N k)) * (w #N ((n + 1) -' k)) by A21, LOPBAN_3:38
.= (Expan ((n + 1),z,w)) . k by A8, Def6 ;
hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k ; :: thesis: verum

end;

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

A22: (n + 1) -' 0 = (n + 1) - 0 by XREAL_1:233;
then A23: (Coef (n + 1)) . 0 = ((n + 1) !) / ((0 !) * ((n + 1) !)) by Def3
.= 1 by NEWTON:12, XCMPLX_1:60 ;
A24: n -' 0 = n - 0 by XREAL_1:233;
then A25: (Coef n) . 0 = (n !) / ((0 !) * (n !)) by Def3
.= 1 by NEWTON:12, XCMPLX_1:60 ;
assume A26: k = 0 ; :: thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
then (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (((Expan (n,z,w)) * w) . 0) + ((Shift ((Expan (n,z,w)) * z)) . 0) by NORMSP_1:def 2
.= (((Expan (n,z,w)) . 0) * w) + ((Shift ((Expan (n,z,w)) * z)) . 0) by LOPBAN_3:def 6
.= (((Expan (n,z,w)) . 0) * w) + (0. X) by Def5
.= ((Expan (n,z,w)) . 0) * w by LOPBAN_3:38
.= ((((Coef n) . 0) * (z #N 0)) * (w #N (n -' 0))) * w by Def6
.= (((Coef n) . 0) * (z #N 0)) * ((w #N (n -' 0)) * w) by LOPBAN_3:38
.= (((Coef (n + 1)) . 0) * (z #N 0)) * (w #N ((n + 1) -' 0)) by A24, A22, A25, A23, Lm1
.= (Expan ((n + 1),z,w)) . k by A26, Def6 ;
hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k ; :: thesis: verum

end;

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

end;

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

A28: (n + 1) -' (n + 1) = (n + 1) - (n + 1) by XREAL_1:233
.= 0 ;
then A29: (Coef (n + 1)) . (n + 1) = ((n + 1) !) / (((n + 1) !) * (0 !)) by Def3
.= 1 by NEWTON:12, XCMPLX_1:60 ;
A30: n -' n = n - n by XREAL_1:233
.= 0 ;
then A31: (Coef n) . n = (n !) / ((n !) * (0 !)) by Def3
.= 1 by NEWTON:12, XCMPLX_1:60 ;
A32: n < n + 1 by XREAL_1:29;
assume A33: k = n + 1 ; :: thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
then (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (((Expan (n,z,w)) * w) . (n + 1)) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1)) by NORMSP_1:def 2
.= (((Expan (n,z,w)) . (n + 1)) * w) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1)) by LOPBAN_3:def 6
.= ((0. X) * w) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1)) by A32, Def6
.= (0. X) + ((Shift ((Expan (n,z,w)) * z)) . (n + 1)) by LOPBAN_3:38
.= (Shift ((Expan (n,z,w)) * z)) . (n + 1) by LOPBAN_3:38
.= ((Expan (n,z,w)) * z) . n by Def5
.= ((Expan (n,z,w)) . n) * z by LOPBAN_3:def 6
.= ((((Coef n) . n) * (z #N n)) * (w #N (n -' n))) * z by Def6
.= (((Coef n) . n) * (z #N n)) * ((w #N (n -' n)) * z) by LOPBAN_3:38
.= (((Coef n) . n) * (z #N n)) * (z * (w #N (n -' n))) by A1, Lm2
.= ((((Coef n) . n) * (z #N n)) * z) * (w #N (n -' n)) by LOPBAN_3:38
.= (((Coef n) . n) * ((z #N n) * z)) * (w #N (n -' n)) by LOPBAN_3:38
.= (((Coef (n + 1)) . (n + 1)) * (z #N (n + 1))) * (w #N (n -' n)) by A31, A29, Lm1
.= (Expan ((n + 1),z,w)) . k by A33, A30, A28, Def6 ;
hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k ; :: thesis: verum

end;

assume k <= n + 1 ; :: thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k by A27, A7, XXREAL_0:1; :: thesis: verum

end;

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

assume A34: n + 1 < k ; :: thesis: (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k
then A35: (n + 1) - 1 < k - 1 by XREAL_1:9;
then A36: n + 0 < (k - 1) + 1 by XREAL_1:8;
0 + 1 <= n + 1 by XREAL_1:6;
then A37: k - 1 = k -' 1 by A34, XREAL_1:233, XXREAL_0:2;
(((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (((Expan (n,z,w)) * w) . k) + ((Shift ((Expan (n,z,w)) * z)) . k) by NORMSP_1:def 2
.= (((Expan (n,z,w)) . k) * w) + ((Shift ((Expan (n,z,w)) * z)) . k) by LOPBAN_3:def 6
.= (((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) * z) . (k -' 1)) by A36, Th15
.= (((Expan (n,z,w)) . k) * w) + (((Expan (n,z,w)) . (k -' 1)) * z) by LOPBAN_3:def 6
.= ((0. X) * w) + (((Expan (n,z,w)) . (k -' 1)) * z) by A36, Def6
.= (0. X) + (((Expan (n,z,w)) . (k -' 1)) * z) by LOPBAN_3:38
.= (0. X) + ((0. X) * z) by A35, A37, Def6
.= (0. X) + (0. X) by LOPBAN_3:38
.= 0. X by LOPBAN_3:38 ;
hence (((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z))) . k = (Expan ((n + 1),z,w)) . k by A34, Def6; :: thesis: verum

end;

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

end;

then A38: ((Expan (n,z,w)) * w) + (Shift ((Expan (n,z,w)) * z)) = Expan ((n + 1),z,w) by FUNCT_2:63;
A39: n < n + 1 by XREAL_1:29;
(Partial_Sums ((Expan (n,z,w)) * w)) . (n + 1) = ((Partial_Sums ((Expan (n,z,w)) * w)) . n) + (((Expan (n,z,w)) * w) . (n + 1)) by BHSP_4:def 1
.= ((Partial_Sums ((Expan (n,z,w)) * w)) . n) + (((Expan (n,z,w)) . (n + 1)) * w) by LOPBAN_3:def 6 ;
then A40: (Partial_Sums ((Expan (n,z,w)) * w)) . (n + 1) = ((Partial_Sums ((Expan (n,z,w)) * w)) . n) + ((0. X) * w) by A39, Def6
.= ((Partial_Sums ((Expan (n,z,w)) * w)) . n) + (0. X) by LOPBAN_3:38
.= (Partial_Sums ((Expan (n,z,w)) * w)) . n by LOPBAN_3:38 ;
(Partial_Sums ((Expan (n,z,w)) * z)) . (n + 1) = ((Partial_Sums ((Expan (n,z,w)) * z)) . n) + (((Expan (n,z,w)) * z) . (n + 1)) by BHSP_4:def 1
.= ((Partial_Sums ((Expan (n,z,w)) * z)) . n) + (((Expan (n,z,w)) . (n + 1)) * z) by LOPBAN_3:def 6 ;
then A41: (Partial_Sums ((Expan (n,z,w)) * z)) . (n + 1) = ((Partial_Sums ((Expan (n,z,w)) * z)) . n) + ((0. X) * z) by A4, Def6
.= ((Partial_Sums ((Expan (n,z,w)) * z)) . n) + (0. X) by LOPBAN_3:38
.= (Partial_Sums ((Expan (n,z,w)) * z)) . n by LOPBAN_3:38 ;
0 + n < n + 1 by XREAL_1:29;
then A42: (Expan (n,z,w)) . (n + 1) = 0. X by Def6;
(Partial_Sums ((Expan (n,z,w)) * z)) . (n + 1) = ((Partial_Sums (Shift ((Expan (n,z,w)) * z))) . (n + 1)) + (((Expan (n,z,w)) * z) . (n + 1)) by Th16;
then A43: (Partial_Sums ((Expan (n,z,w)) * z)) . (n + 1) = ((Partial_Sums (Shift ((Expan (n,z,w)) * z))) . (n + 1)) + (((Expan (n,z,w)) . (n + 1)) * z) by LOPBAN_3:def 6
.= ((Partial_Sums (Shift ((Expan (n,z,w)) * z))) . (n + 1)) + (0. X) by A42, LOPBAN_3:38
.= (Partial_Sums (Shift ((Expan (n,z,w)) * z))) . (n + 1) by LOPBAN_3:38 ;

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

let k be Element of NAT ; :: thesis: ((Expan (n,z,w)) * (z + w)) . k = (((Expan (n,z,w)) * z) + ((Expan (n,z,w)) * w)) . k
thus ((Expan (n,z,w)) * (z + w)) . k = ((Expan (n,z,w)) . k) * (z + w) by LOPBAN_3:def 6
.= (((Expan (n,z,w)) . k) * z) + (((Expan (n,z,w)) . k) * w) by LOPBAN_3:38
.= (((Expan (n,z,w)) * z) . k) + (((Expan (n,z,w)) . k) * w) by LOPBAN_3:def 6
.= (((Expan (n,z,w)) * z) . k) + (((Expan (n,z,w)) * w) . k) by LOPBAN_3:def 6
.= (((Expan (n,z,w)) * z) + ((Expan (n,z,w)) * w)) . k by NORMSP_1:def 2 ; :: thesis: verum

end;

then A44: (Expan (n,z,w)) * (z + w) = ((Expan (n,z,w)) * z) + ((Expan (n,z,w)) * w) by FUNCT_2:63;
(z + w) #N (n + 1) = (((z + w) GeoSeq) . n) * (z + w) by LOPBAN_3:def 9
.= ((Partial_Sums (Expan (n,z,w))) * (z + w)) . n by A3, LOPBAN_3:def 6
.= (Partial_Sums ((Expan (n,z,w)) * (z + w))) . n by Th9 ;
then (z + w) #N (n + 1) = ((Partial_Sums ((Expan (n,z,w)) * z)) + (Partial_Sums ((Expan (n,z,w)) * w))) . n by A44, LOPBAN_3:15
.= ((Partial_Sums ((Expan (n,z,w)) * z)) . n) + ((Partial_Sums ((Expan (n,z,w)) * w)) . n) by NORMSP_1:def 2 ;
hence (z + w) #N (n + 1) = ((Partial_Sums ((Expan (n,z,w)) * w)) + (Partial_Sums (Shift ((Expan (n,z,w)) * z)))) . (n + 1) by A41, A40, A43, NORMSP_1:def 2
.= (Partial_Sums (Expan ((n + 1),z,w))) . (n + 1) by A38, LOPBAN_3:15 ;
:: thesis: verum

end;

A45: 0 -' 0 = 0 - 0 by XREAL_0:def 2
.= 0 ;
(Partial_Sums (Expan (0,z,w))) . 0 = (Expan (0,z,w)) . 0 by BHSP_4:def 1
.= (((Coef 0) . 0) * (z #N 0)) * (w #N 0) by A45, Def6
.= ((1 / (1 * 1)) * (z #N 0)) * (w #N 0) by A45, Def3, NEWTON:12
.= ((z GeoSeq) . 0) * (w #N 0) by RLVECT_1:def 8
.= (1. X) * ((w GeoSeq) . 0) by LOPBAN_3:def 9
.= (1. X) * (1. X) by LOPBAN_3:def 9
.= 1. X by LOPBAN_3:38 ;
then A46: S₁[ 0 ] by LOPBAN_3:def 9;
for n being Nat holds S₁[n] from NAT_1:sch 2(A46, A2);
hence (z + w) #N n = (Partial_Sums (Expan (n,z,w))) . n ; :: thesis: verum