clopban4.miz

begin

 reserve X for Complex_Banach_Algebra,

w,z,z1,z2 for Element of X,

k,l,m,n,n1,n2 for Nat,

seq,seq1,seq2,s,s9 for sequence of X,

rseq for Real_Sequence;



 Lm1: (z * (z #N n)) = (z #N (n + 1)) & ((z #N n) * z) = (z #N (n + 1)) & (z * (z #N n)) = ((z #N n) * z)

 proof

 defpred P[ Nat] means (z * (z #N $1)) = (z #N ($1 + 1));



 A1: (z #N ( 0 + 1)) = ((z GeoSeq ) . ( 0 + 1)) by CLOPBAN3:def 8

 .= (((z GeoSeq ) . 0 ) * z) by CLOPBAN3:def 7

 .= (( 1. X) * z) by CLOPBAN3:def 7

 .= z by VECTSP_1:def 8;



 A2: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat such that

 A3: P[k];



 thus (z * (z #N (k + 1))) = (z * ((z GeoSeq ) . (k + 1))) by CLOPBAN3:def 8

 .= (z * (((z GeoSeq ) . k) * z)) by CLOPBAN3:def 7

 .= (z * ((z #N k) * z)) by CLOPBAN3:def 8

 .= ((z * (z #N k)) * z) by GROUP_1:def 3

 .= (((z GeoSeq ) . (k + 1)) * z) by A3, CLOPBAN3:def 8

 .= ((z GeoSeq ) . ((k + 1) + 1)) by CLOPBAN3:def 7

 .= (z #N ((k + 1) + 1)) by CLOPBAN3:def 8;

 end;

 (z * (z #N 0 )) = (z * ((z GeoSeq ) . 0 )) by CLOPBAN3:def 8

 .= (z * ( 1. X)) by CLOPBAN3:def 7

 .= z by VECTSP_1:def 4;

 then

 A4: P[ 0 ] by A1;



 A5: for n be Nat holds P[n] from NAT_1:sch 2( A4, A2);

 now

 let n;

 thus (z * (z #N n)) = (z #N (n + 1)) by A5;



 thus ((z #N n) * z) = (((z GeoSeq ) . n) * z) by CLOPBAN3:def 8

 .= ((z GeoSeq ) . (n + 1)) by CLOPBAN3:def 7

 .= (z #N (n + 1)) by CLOPBAN3:def 8;

 hence (z * (z #N n)) = ((z #N n) * z) by A5;

 end;

 hence thesis;

 end;



 Lm2: for z, w st (z,w) are_commutative holds (w * (z #N n)) = ((z #N n) * w) & (z * (w #N n)) = ((w #N n) * z)

 proof

 let z, w such that

 A1: (z,w) are_commutative ;

 defpred P[ Nat] means (w * (z #N $1)) = ((z #N $1) * w) & (z * (w #N $1)) = ((w #N $1) * z);



 A2: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat such that

 A3: P[k];



 A4: (z * (w #N (k + 1))) = (z * ((w #N k) * w)) by Lm1

 .= ((z * (w #N k)) * w) by GROUP_1:def 3

 .= ((w #N k) * (z * w)) by A3, GROUP_1:def 3

 .= ((w #N k) * (w * z)) by A1, LOPBAN_4:def 1

 .= (((w #N k) * w) * z) by GROUP_1:def 3

 .= ((w #N (k + 1)) * z) by Lm1;

 (w * (z #N (k + 1))) = (w * ((z #N k) * z)) by Lm1

 .= ((w * (z #N k)) * z) by GROUP_1:def 3

 .= ((z #N k) * (w * z)) by A3, GROUP_1:def 3

 .= ((z #N k) * (z * w)) by A1, LOPBAN_4:def 1

 .= (((z #N k) * z) * w) by GROUP_1:def 3

 .= ((z #N (k + 1)) * w) by Lm1;

 hence thesis by A4;

 end;



 A5: (w #N 0 ) = ((w GeoSeq ) . 0 ) by CLOPBAN3:def 8

 .= ( 1. X) by CLOPBAN3:def 7;



 then

 A6: (z * (w #N 0 )) = z by VECTSP_1:def 4

 .= ((w #N 0 ) * z) by A5, VECTSP_1:def 8;



 A7: (z #N 0 ) = ((z GeoSeq ) . 0 ) by CLOPBAN3:def 8

 .= ( 1. X) by CLOPBAN3:def 7;



 then (w * (z #N 0 )) = w by VECTSP_1:def 4

 .= ((z #N 0 ) * w) by A7, VECTSP_1:def 8;

 then

 A8: P[ 0 ] by A6;

 for n be Nat holds P[n] from NAT_1:sch 2( A8, A2);

 hence thesis;

 end;

 theorem :: CLOPBAN4:1



 Th1: seq1 is convergent & seq2 is convergent & ( lim (seq1 - seq2)) = ( 0. X) implies ( lim seq1) = ( lim seq2)

 proof

 assume that

 A1: seq1 is convergent and

 A2: seq2 is convergent and

 A3: ( lim (seq1 - seq2)) = ( 0. X);

 (( lim seq1) - ( lim seq2)) = ( 0. X) by A1, A2, A3, CLVECT_1: 120;

 then ((( lim seq1) - ( lim seq2)) + ( lim seq2)) = ( lim seq2) by RLVECT_1:def 4;

 then (( lim seq1) - (( lim seq2) - ( lim seq2))) = ( lim seq2) by CLOPBAN3: 38;

 then (( lim seq1) - ( 0. X)) = ( lim seq2) by RLVECT_1: 15;

 hence thesis by RLVECT_1: 13;

 end;

 theorem :: CLOPBAN4:2



 Th2: for z st for n be Nat holds (s . n) = z holds ( lim s) = z

 proof

 let z;

 assume

 A1: for n be Nat holds (s . n) = z;

 A2:

 now

 let p be Real such that

 A3: 0 < p;

 reconsider k = 0 as Nat;

 take k;

 let n such that k <= n;

 (s . n) = z by A1;

 hence ||.((s . n) - z).|| < p by A3, CLVECT_1: 107;

 end;

 then s is convergent;

 hence thesis by A2, CLVECT_1:def 16;

 end;

 theorem :: CLOPBAN4:3



 Th3: s is convergent & s9 is convergent implies (s * s9) is convergent

 proof

 assume that

 A1: s is convergent and

 A2: s9 is convergent;

 consider g1 be Point of X such that

 A3: for p be Real st 0 < p holds ex n st for m st n <= m holds ||.((s . m) - g1).|| < p by A1;

 ||.s.|| is bounded by A1, CLVECT_1: 117, SEQ_2: 13;

 then

 consider R be Real such that

 A4: for n holds ( ||.s.|| . n) < R by SEQ_2:def 3;

 A5:

 now

 let n;

 ||.(s . n).|| = ( ||.s.|| . n) by NORMSP_0:def 4;

 hence ||.(s . n).|| < R by A4;

 end;

 ||.(s . 1).|| = ( ||.s.|| . 1) by NORMSP_0:def 4;

 then 0 <= ( ||.s.|| . 1) by CLVECT_1: 105;

 then

 A6: 0 < R by A4;

 consider g2 be Point of X such that

 A7: for p be Real st 0 < p holds ex n st for m st n <= m holds ||.((s9 . m) - g2).|| < p by A2;

 take g = (g1 * g2);

 let p be Real;

 reconsider R as Real;



 A8: ( 0 + 0 ) < ( ||.g2.|| + R) by A6, CLVECT_1: 105, XREAL_1: 8;

 assume

 A9: 0 < p;

 then

 consider n1 such that

 A10: for m st n1 <= m holds ||.((s . m) - g1).|| < (p / ( ||.g2.|| + R)) by A3, A8;

 consider n2 such that

 A11: for m st n2 <= m holds ||.((s9 . m) - g2).|| < (p / ( ||.g2.|| + R)) by A7, A8, A9;

 take n = (n1 + n2);

 let m such that

 A12: n <= m;

 n2 <= n by NAT_1: 12;

 then n2 <= m by A12, XXREAL_0: 2;

 then

 A13: ||.((s9 . m) - g2).|| < (p / ( ||.g2.|| + R)) by A11;



 A14: 0 <= ||.(s . m).|| by CLVECT_1: 105;



 A15: ||.((s . m) * ((s9 . m) - g2)).|| <= ( ||.(s . m).|| * ||.((s9 . m) - g2).||) by CLOPBAN3: 38;



 A16: 0 <= ||.((s9 . m) - g2).|| by CLVECT_1: 105;

 n1 <= (n1 + n2) by NAT_1: 12;

 then n1 <= m by A12, XXREAL_0: 2;

 then

 A17: ||.((s . m) - g1).|| <= (p / ( ||.g2.|| + R)) by A10;

 ||.(((s * s9) . m) - g).|| = ||.(((s . m) * (s9 . m)) - (g1 * g2)).|| by LOPBAN_3:def 7

 .= ||.((((s . m) * (s9 . m)) - ((s . m) * g2)) + (((s . m) * g2) - (g1 * g2))).|| by CLOPBAN3: 38

 .= ||.(((s . m) * ((s9 . m) - g2)) + (((s . m) * g2) - (g1 * g2))).|| by CLOPBAN3: 38

 .= ||.(((s . m) * ((s9 . m) - g2)) + (((s . m) - g1) * g2)).|| by CLOPBAN3: 38;

 then

 A18: ||.(((s * s9) . m) - g).|| <= ( ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).||) by CLVECT_1:def 13;

 ||.(s . m).|| < R by A5;

 then ( ||.(s . m).|| * ||.((s9 . m) - g2).||) < (R * (p / ( ||.g2.|| + R))) by A14, A16, A13, XREAL_1: 96;

 then

 A19: ||.((s . m) * ((s9 . m) - g2)).|| < (R * (p / ( ||.g2.|| + R))) by A15, XXREAL_0: 2;



 A20: ||.(((s . m) - g1) * g2).|| <= ( ||.g2.|| * ||.((s . m) - g1).||) by CLOPBAN3: 38;

 0 <= ||.g2.|| by CLVECT_1: 105;

 then ( ||.g2.|| * ||.((s . m) - g1).||) <= ( ||.g2.|| * (p / ( ||.g2.|| + R))) by A17, XREAL_1: 64;

 then

 A21: ||.(((s . m) - g1) * g2).|| <= ( ||.g2.|| * (p / ( ||.g2.|| + R))) by A20, XXREAL_0: 2;

 ((R * (p / ( ||.g2.|| + R))) + ( ||.g2.|| * (p / ( ||.g2.|| + R)))) = ((p / ( ||.g2.|| + R)) * ( ||.g2.|| + R))

 .= p by A8, XCMPLX_1: 87;

 then ( ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).||) < p by A19, A21, XREAL_1: 8;

 hence thesis by A18, XXREAL_0: 2;

 end;

 theorem :: CLOPBAN4:4



 Th4: s is convergent implies (z * s) is convergent

 proof



 A1: 0 <= ||.z.|| by CLVECT_1: 105;

 assume s is convergent;

 then

 consider g1 be Point of X such that

 A2: for p be Real st 0 < p holds ex n st for m st n <= m holds ||.((s . m) - g1).|| < p;

 take g = (z * g1);

 let p be Real;

 assume

 A3: 0 < p;



 A4: ( 0 + 0 ) < ( ||.z.|| + 1) by CLVECT_1: 105, XREAL_1: 8;

 then

 consider n such that

 A5: for m st n <= m holds ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A2, A3;

 take n;

 let m;

 assume n <= m;

 then

 A6: ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A5;



 A7: ||.(z * ((s . m) - g1)).|| <= ( ||.z.|| * ||.((s . m) - g1).||) by CLOPBAN3: 38;

 0 <= ||.((s . m) - g1).|| by CLVECT_1: 105;

 then ( ||.z.|| * ||.((s . m) - g1).||) <= ( ||.z.|| * (p / ( ||.z.|| + 1))) by A1, A6, XREAL_1: 66;

 then

 A8: ||.(z * ((s . m) - g1)).|| <= ( ||.z.|| * (p / ( ||.z.|| + 1))) by A7, XXREAL_0: 2;



 A9: ||.(((z * s) . m) - g).|| = ||.((z * (s . m)) - (z * g1)).|| by LOPBAN_3:def 5

 .= ||.(z * ((s . m) - g1)).|| by CLOPBAN3: 38;

 ( 0 + ||.z.||) < ( ||.z.|| + 1) by XREAL_1: 8;

 then

 A10: ( ||.z.|| * (p / ( ||.z.|| + 1))) < (( ||.z.|| + 1) * (p / ( ||.z.|| + 1))) by A1, A3, XREAL_1: 97;

 (( ||.z.|| + 1) * (p / ( ||.z.|| + 1))) = p by A4, XCMPLX_1: 87;

 hence thesis by A9, A8, A10, XXREAL_0: 2;

 end;

 theorem :: CLOPBAN4:5



 Th5: s is convergent implies (s * z) is convergent

 proof



 A1: 0 <= ||.z.|| by CLVECT_1: 105;

 assume s is convergent;

 then

 consider g1 be Point of X such that

 A2: for p be Real st 0 < p holds ex n st for m st n <= m holds ||.((s . m) - g1).|| < p;

 take g = (g1 * z);

 let p be Real;

 assume

 A3: 0 < p;



 A4: ( 0 + 0 ) < ( ||.z.|| + 1) by CLVECT_1: 105, XREAL_1: 8;

 then

 consider n such that

 A5: for m st n <= m holds ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A2, A3;

 take n;

 let m;

 assume n <= m;

 then

 A6: ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A5;



 A7: ||.(((s . m) - g1) * z).|| <= ( ||.((s . m) - g1).|| * ||.z.||) by CLOPBAN3: 38;

 0 <= ||.((s . m) - g1).|| by CLVECT_1: 105;

 then ( ||.((s . m) - g1).|| * ||.z.||) <= ((p / ( ||.z.|| + 1)) * ||.z.||) by A1, A6, XREAL_1: 66;

 then

 A8: ||.(((s . m) - g1) * z).|| <= ((p / ( ||.z.|| + 1)) * ||.z.||) by A7, XXREAL_0: 2;



 A9: ||.(((s * z) . m) - g).|| = ||.(((s . m) * z) - (g1 * z)).|| by LOPBAN_3:def 6

 .= ||.(((s . m) - g1) * z).|| by CLOPBAN3: 38;

 ( 0 + ||.z.||) < ( ||.z.|| + 1) by XREAL_1: 8;

 then

 A10: ((p / ( ||.z.|| + 1)) * ||.z.||) < ((p / ( ||.z.|| + 1)) * ( ||.z.|| + 1)) by A1, A3, XREAL_1: 97;

 ((p / ( ||.z.|| + 1)) * ( ||.z.|| + 1)) = p by A4, XCMPLX_1: 87;

 hence thesis by A9, A8, A10, XXREAL_0: 2;

 end;

 theorem :: CLOPBAN4:6



 Th6: s is convergent implies ( lim (z * s)) = (z * ( lim s))

 proof

 assume

 A1: s is convergent;

 set g1 = ( lim s);

 set g = (z * g1);



 A2: ( 0 + 0 ) < ( ||.z.|| + 1) by CLVECT_1: 105, XREAL_1: 8;



 A3: 0 <= ||.z.|| by CLVECT_1: 105;

 A4:

 now

 let p be Real;

 assume

 A5: 0 < p;

 then

 consider n such that

 A6: for m st n <= m holds ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A1, A2, CLVECT_1:def 16;

 take n;

 let m;

 assume n <= m;

 then

 A7: ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A6;

 0 <= ||.((s . m) - g1).|| by CLVECT_1: 105;

 then

 A8: ( ||.z.|| * ||.((s . m) - g1).||) <= ( ||.z.|| * (p / ( ||.z.|| + 1))) by A3, A7, XREAL_1: 66;

 ||.(z * ((s . m) - g1)).|| <= ( ||.z.|| * ||.((s . m) - g1).||) by CLOPBAN3: 38;

 then

 A9: ||.(z * ((s . m) - g1)).|| <= ( ||.z.|| * (p / ( ||.z.|| + 1))) by A8, XXREAL_0: 2;



 A10: ||.(((z * s) . m) - g).|| = ||.((z * (s . m)) - (z * g1)).|| by LOPBAN_3:def 5

 .= ||.(z * ((s . m) - g1)).|| by CLOPBAN3: 38;

 ( 0 + ||.z.||) < ( ||.z.|| + 1) by XREAL_1: 8;

 then

 A11: ( ||.z.|| * (p / ( ||.z.|| + 1))) < (( ||.z.|| + 1) * (p / ( ||.z.|| + 1))) by A3, A5, XREAL_1: 97;

 (( ||.z.|| + 1) * (p / ( ||.z.|| + 1))) = p by A2, XCMPLX_1: 87;

 hence ||.(((z * s) . m) - g).|| < p by A10, A9, A11, XXREAL_0: 2;

 end;

 (z * s) is convergent by A1, Th4;

 hence thesis by A4, CLVECT_1:def 16;

 end;

 theorem :: CLOPBAN4:7



 Th7: s is convergent implies ( lim (s * z)) = (( lim s) * z)

 proof

 assume

 A1: s is convergent;

 set g1 = ( lim s);

 set g = (g1 * z);



 A2: ( 0 + 0 ) < ( ||.z.|| + 1) by CLVECT_1: 105, XREAL_1: 8;



 A3: 0 <= ||.z.|| by CLVECT_1: 105;

 A4:

 now

 let p be Real;

 assume

 A5: 0 < p;

 then

 consider n such that

 A6: for m st n <= m holds ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A1, A2, CLVECT_1:def 16;

 take n;

 let m;

 assume n <= m;

 then

 A7: ||.((s . m) - g1).|| < (p / ( ||.z.|| + 1)) by A6;

 0 <= ||.((s . m) - g1).|| by CLVECT_1: 105;

 then

 A8: ( ||.((s . m) - g1).|| * ||.z.||) <= ((p / ( ||.z.|| + 1)) * ||.z.||) by A3, A7, XREAL_1: 66;

 ||.(((s . m) - g1) * z).|| <= ( ||.((s . m) - g1).|| * ||.z.||) by CLOPBAN3: 38;

 then

 A9: ||.(((s . m) - g1) * z).|| <= ((p / ( ||.z.|| + 1)) * ||.z.||) by A8, XXREAL_0: 2;



 A10: ||.(((s * z) . m) - g).|| = ||.(((s . m) * z) - (g1 * z)).|| by LOPBAN_3:def 6

 .= ||.(((s . m) - g1) * z).|| by CLOPBAN3: 38;

 ( 0 + ||.z.||) < ( ||.z.|| + 1) by XREAL_1: 8;

 then

 A11: ((p / ( ||.z.|| + 1)) * ||.z.||) < ((p / ( ||.z.|| + 1)) * ( ||.z.|| + 1)) by A3, A5, XREAL_1: 97;

 ((p / ( ||.z.|| + 1)) * ( ||.z.|| + 1)) = p by A2, XCMPLX_1: 87;

 hence ||.(((s * z) . m) - g).|| < p by A10, A9, A11, XXREAL_0: 2;

 end;

 (s * z) is convergent by A1, Th5;

 hence thesis by A4, CLVECT_1:def 16;

 end;

 theorem :: CLOPBAN4:8



 Th8: s is convergent & s9 is convergent implies ( lim (s * s9)) = (( lim s) * ( lim s9))

 proof

 assume that

 A1: s is convergent and

 A2: s9 is convergent;

 ||.s.|| is bounded by A1, CLVECT_1: 117, SEQ_2: 13;

 then

 consider R be Real such that

 A3: for n holds ( ||.s.|| . n) < R by SEQ_2:def 3;

 set g2 = ( lim s9);

 set g1 = ( lim s);

 set g = (g1 * g2);

 A4:

 now

 let n;

 ||.(s . n).|| = ( ||.s.|| . n) by NORMSP_0:def 4;

 hence ||.(s . n).|| < R by A3;

 end;

 ||.(s . 1).|| = ( ||.s.|| . 1) by NORMSP_0:def 4;

 then 0 <= ( ||.s.|| . 1) by CLVECT_1: 105;

 then

 A5: 0 < R by A3;

 reconsider R as Real;



 A6: ( 0 + 0 ) < ( ||.g2.|| + R) by A5, CLVECT_1: 105, XREAL_1: 8;



 A7: 0 <= ||.g2.|| by CLVECT_1: 105;

 A8:

 now

 let p be Real;

 assume

 A9: 0 < p;

 then

 consider n1 such that

 A10: for m st n1 <= m holds ||.((s . m) - g1).|| < (p / ( ||.g2.|| + R)) by A1, A6, CLVECT_1:def 16;

 consider n2 such that

 A11: for m st n2 <= m holds ||.((s9 . m) - g2).|| < (p / ( ||.g2.|| + R)) by A2, A6, A9, CLVECT_1:def 16;

 take n = (n1 + n2);

 let m such that

 A12: n <= m;

 n1 <= (n1 + n2) by NAT_1: 12;

 then n1 <= m by A12, XXREAL_0: 2;

 then ||.((s . m) - g1).|| <= (p / ( ||.g2.|| + R)) by A10;

 then

 A13: ( ||.g2.|| * ||.((s . m) - g1).||) <= ( ||.g2.|| * (p / ( ||.g2.|| + R))) by A7, XREAL_1: 64;

 ||.(((s . m) - g1) * g2).|| <= ( ||.g2.|| * ||.((s . m) - g1).||) by CLOPBAN3: 38;

 then

 A14: ||.(((s . m) - g1) * g2).|| <= ( ||.g2.|| * (p / ( ||.g2.|| + R))) by A13, XXREAL_0: 2;



 A15: 0 <= ||.(s . m).|| by CLVECT_1: 105;

 ||.(((s * s9) . m) - g).|| = ||.(((s . m) * (s9 . m)) - (g1 * g2)).|| by LOPBAN_3:def 7

 .= ||.((((s . m) * (s9 . m)) - ((s . m) * g2)) + (((s . m) * g2) - (g1 * g2))).|| by CLOPBAN3: 38

 .= ||.(((s . m) * ((s9 . m) - g2)) + (((s . m) * g2) - (g1 * g2))).|| by CLOPBAN3: 38

 .= ||.(((s . m) * ((s9 . m) - g2)) + (((s . m) - g1) * g2)).|| by CLOPBAN3: 38;

 then

 A16: ||.(((s * s9) . m) - g).|| <= ( ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).||) by CLVECT_1:def 13;



 A17: ||.((s . m) * ((s9 . m) - g2)).|| <= ( ||.(s . m).|| * ||.((s9 . m) - g2).||) by CLOPBAN3: 38;

 n2 <= n by NAT_1: 12;

 then n2 <= m by A12, XXREAL_0: 2;

 then

 A18: ||.((s9 . m) - g2).|| < (p / ( ||.g2.|| + R)) by A11;



 A19: 0 <= ||.((s9 . m) - g2).|| by CLVECT_1: 105;

 ||.(s . m).|| < R by A4;

 then ( ||.(s . m).|| * ||.((s9 . m) - g2).||) < (R * (p / ( ||.g2.|| + R))) by A15, A19, A18, XREAL_1: 96;

 then

 A20: ||.((s . m) * ((s9 . m) - g2)).|| < (R * (p / ( ||.g2.|| + R))) by A17, XXREAL_0: 2;

 ((R * (p / ( ||.g2.|| + R))) + ( ||.g2.|| * (p / ( ||.g2.|| + R)))) = ((p / ( ||.g2.|| + R)) * ( ||.g2.|| + R))

 .= p by A6, XCMPLX_1: 87;

 then ( ||.((s . m) * ((s9 . m) - g2)).|| + ||.(((s . m) - g1) * g2).||) < p by A20, A14, XREAL_1: 8;

 hence ||.(((s * s9) . m) - g).|| < p by A16, XXREAL_0: 2;

 end;

 (s * s9) is convergent by A1, A2, Th3;

 hence thesis by A8, CLVECT_1:def 16;

 end;

 theorem :: CLOPBAN4:9



 Th9: ( Partial_Sums (z * seq)) = (z * ( Partial_Sums seq)) & ( Partial_Sums (seq * z)) = (( Partial_Sums seq) * z)

 proof



 A1: ( Partial_Sums (seq * z)) = (( Partial_Sums seq) * z)

 proof

 defpred P[ Nat] means (( Partial_Sums (seq * z)) . $1) = ((( Partial_Sums seq) * z) . $1);

 A2:

 now

 let n;

 assume

 A3: P[n];

 (( Partial_Sums (seq * z)) . (n + 1)) = ((( Partial_Sums (seq * z)) . n) + ((seq * z) . (n + 1))) by BHSP_4:def 1

 .= (((( Partial_Sums seq) . n) * z) + ((seq * z) . (n + 1))) by A3, LOPBAN_3:def 6

 .= (((( Partial_Sums seq) . n) * z) + ((seq . (n + 1)) * z)) by LOPBAN_3:def 6

 .= (((( Partial_Sums seq) . n) + (seq . (n + 1))) * z) by VECTSP_1:def 3

 .= ((( Partial_Sums seq) . (n + 1)) * z) by BHSP_4:def 1

 .= ((( Partial_Sums seq) * z) . (n + 1)) by LOPBAN_3:def 6;

 hence P[(n + 1)];

 end;

 (( Partial_Sums (seq * z)) . 0 ) = ((seq * z) . 0 ) by BHSP_4:def 1

 .= ((seq . 0 ) * z) by LOPBAN_3:def 6

 .= ((( Partial_Sums seq) . 0 ) * z) by BHSP_4:def 1

 .= ((( Partial_Sums seq) * z) . 0 ) by LOPBAN_3:def 6;

 then

 A4: P[ 0 ];

 for n holds P[n] from NAT_1:sch 2( A4, A2);

 then for n be Element of NAT holds P[n];

 hence thesis by FUNCT_2: 63;

 end;

 ( Partial_Sums (z * seq)) = (z * ( Partial_Sums seq))

 proof

 defpred P[ Nat] means (( Partial_Sums (z * seq)) . $1) = ((z * ( Partial_Sums seq)) . $1);

 A5:

 now

 let n;

 assume

 A6: P[n];

 (( Partial_Sums (z * seq)) . (n + 1)) = ((( Partial_Sums (z * seq)) . n) + ((z * seq) . (n + 1))) by BHSP_4:def 1

 .= ((z * (( Partial_Sums seq) . n)) + ((z * seq) . (n + 1))) by A6, LOPBAN_3:def 5

 .= ((z * (( Partial_Sums seq) . n)) + (z * (seq . (n + 1)))) by LOPBAN_3:def 5

 .= (z * ((( Partial_Sums seq) . n) + (seq . (n + 1)))) by VECTSP_1:def 2

 .= (z * (( Partial_Sums seq) . (n + 1))) by BHSP_4:def 1

 .= ((z * ( Partial_Sums seq)) . (n + 1)) by LOPBAN_3:def 5;

 hence P[(n + 1)];

 end;

 (( Partial_Sums (z * seq)) . 0 ) = ((z * seq) . 0 ) by BHSP_4:def 1

 .= (z * (seq . 0 )) by LOPBAN_3:def 5

 .= (z * (( Partial_Sums seq) . 0 )) by BHSP_4:def 1

 .= ((z * ( Partial_Sums seq)) . 0 ) by LOPBAN_3:def 5;

 then

 A7: P[ 0 ];

 for n holds P[n] from NAT_1:sch 2( A7, A5);

 then for n be Element of NAT holds P[n];

 hence thesis by FUNCT_2: 63;

 end;

 hence thesis by A1;

 end;

 theorem :: CLOPBAN4:10



 Th10: ||.(( Partial_Sums seq) . k).|| <= (( Partial_Sums ||.seq.||) . k)

 proof

 defpred P[ Nat] means ||.(( Partial_Sums seq) . $1).|| <= (( Partial_Sums ||.seq.||) . $1);

 A1:

 now

 let k;

 assume P[k];

 then

 A2: ( ||.(( Partial_Sums seq) . k).|| + ||.(seq . (k + 1)).||) <= ((( Partial_Sums ||.seq.||) . k) + ||.(seq . (k + 1)).||) by XREAL_1: 6;



 A3: ||.((( Partial_Sums seq) . k) + (seq . (k + 1))).|| <= ( ||.(( Partial_Sums seq) . k).|| + ||.(seq . (k + 1)).||) by CLVECT_1:def 13;

 ||.(( Partial_Sums seq) . (k + 1)).|| = ||.((( Partial_Sums seq) . k) + (seq . (k + 1))).|| by BHSP_4:def 1;

 then ||.(( Partial_Sums seq) . (k + 1)).|| <= ((( Partial_Sums ||.seq.||) . k) + ||.(seq . (k + 1)).||) by A3, A2, XXREAL_0: 2;

 then ||.(( Partial_Sums seq) . (k + 1)).|| <= ((( Partial_Sums ||.seq.||) . k) + ( ||.seq.|| . (k + 1))) by NORMSP_0:def 4;

 hence P[(k + 1)] by SERIES_1:def 1;

 end;

 (( Partial_Sums ||.seq.||) . 0 ) = ( ||.seq.|| . 0 ) by SERIES_1:def 1

 .= ||.(seq . 0 ).|| by NORMSP_0:def 4;

 then

 A4: P[ 0 ] by BHSP_4:def 1;

 for k holds P[k] from NAT_1:sch 2( A4, A1);

 hence thesis;

 end;

 theorem :: CLOPBAN4:11



 Th11: (for n st n <= m holds (seq1 . n) = (seq2 . n)) implies (( Partial_Sums seq1) . m) = (( Partial_Sums seq2) . m)

 proof

 defpred P[ Nat] means $1 <= m implies (( Partial_Sums seq1) . $1) = (( Partial_Sums seq2) . $1);

 assume

 A1: for n st n <= m holds (seq1 . n) = (seq2 . n);



 A2: for k be Nat st P[k] holds P[(k + 1)]

 proof

 let k be Nat such that

 A3: P[k];

 assume

 A4: (k + 1) <= m;

 k < (k + 1) by XREAL_1: 29;



 hence (( Partial_Sums seq1) . (k + 1)) = ((( Partial_Sums seq2) . k) + (seq1 . (k + 1))) by A3, A4, BHSP_4:def 1, XXREAL_0: 2

 .= ((( Partial_Sums seq2) . k) + (seq2 . (k + 1))) by A1, A4

 .= (( Partial_Sums seq2) . (k + 1)) by BHSP_4:def 1;

 end;



 A5: P[ 0 ]

 proof

 assume 0 <= m;



 thus (( Partial_Sums seq1) . 0 ) = (seq1 . 0 ) by BHSP_4:def 1

 .= (seq2 . 0 ) by A1

 .= (( Partial_Sums seq2) . 0 ) by BHSP_4:def 1;

 end;

 for k holds P[k] from NAT_1:sch 2( A5, A2);

 hence thesis;

 end;

 theorem :: CLOPBAN4:12



 Th12: (for n holds ||.(seq . n).|| <= (rseq . n)) & rseq is convergent & ( lim rseq) = 0 implies seq is convergent & ( lim seq) = ( 0. X)

 proof

 assume that

 A1: for n holds ||.(seq . n).|| <= (rseq . n) and

 A2: rseq is convergent and

 A3: ( lim rseq) = 0 ;

 now

 let p be Real;

 assume 0 < p;

 then

 consider n such that

 A4: for m st n <= m holds |.((rseq . m) - 0 ).| < p by A2, A3, SEQ_2:def 7;

 now

 let m;

 assume n <= m;

 then

 A5: |.((rseq . m) - 0 ).| < p by A4;



 A6: ||.((seq . m) - ( 0. X)).|| = ||.(seq . m).|| by RLVECT_1: 13;



 A7: (rseq . m) <= |.(rseq . m).| by ABSVALUE: 4;

 ||.(seq . m).|| <= (rseq . m) by A1;

 then ||.((seq . m) - ( 0. X)).|| <= |.(rseq . m).| by A6, A7, XXREAL_0: 2;

 hence ||.((seq . m) - ( 0. X)).|| < p by A5, XXREAL_0: 2;

 end;

 hence ex n st for m st n <= m holds ||.((seq . m) - ( 0. X)).|| < p;

 end;

 then

 A8: for p be Real st 0 < p holds ex n st for m st n <= m holds ||.((seq . m) - ( 0. X)).|| < p;

 hence seq is convergent;

 hence thesis by A8, CLVECT_1:def 16;

 end;

 definition

 let X, z;

 :: CLOPBAN4:def1

 func z ExpSeq -> sequence of X means

 : Def1: for n holds (it . n) = (( 1r / (n ! )) * (z #N n));

 existence

 proof

 deffunc U( Nat) = (( 1r / ($1 ! )) * (z #N $1));

 consider s be sequence of X such that

 A1: for n be Element of NAT holds (s . n) = U(n) from FUNCT_2:sch 4;

 take s;

 let n be Nat;

 n in NAT by ORDINAL1:def 12;

 hence thesis by A1;

 end;

 uniqueness

 proof

 let S1,S2 be sequence of X;

 assume that

 A2: for n be Nat holds (S1 . n) = (( 1r / (n ! )) * (z #N n)) and

 A3: for n be Nat holds (S2 . n) = (( 1r / (n ! )) * (z #N n));

 for n be Element of NAT holds (S1 . n) = (S2 . n)

 proof

 let n be Element of NAT ;

 (S1 . n) = (( 1r / (n ! )) * (z #N n)) by A2;

 hence thesis by A3;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 end

 scheme :: CLOPBAN4:sch1

 ExNormSpaceCASE { CNS() -> non empty Complex_Banach_Algebra , F( Nat, Nat) -> Point of CNS() } :

for k holds ex seq be sequence of CNS() st for n holds (n <= k implies (seq . n) = F(k,n)) & (n > k implies (seq . n) = ( 0. CNS()));

 let k;

 defpred P[ object, object] means ex n st (n = $1 & (n <= k implies $2 = F(k,n)) & (n > k implies $2 = ( 0. CNS())));

 A1:

 now

 let x be object;

 assume x in NAT ;

 then

 consider n such that

 A2: n = x;

 reconsider y = (( CHK (n,k)) * F(k,n)) as object;



 A3: n > k implies (( CHK (n,k)) * F(k,n)) = ( 0. CNS()) by CLVECT_1: 1, SIN_COS:def 1;

 take y;

 now

 assume n <= k;



 hence (( CHK (n,k)) * F(k,n)) = ( 1r * F(k,n)) by COMPLEX1:def 4, SIN_COS:def 1

 .= F(k,n) by CLVECT_1:def 5;

 end;

 hence P[x, y] by A2, A3;

 end;

 consider f be Function such that

 A4: ( dom f) = NAT and

 A5: for x be object st x in NAT holds P[x, (f . x)] from CLASSES1:sch 1( A1);

 now

 let x be object;

 assume x in NAT ;

 then ex n st n = x & (n <= k implies (f . x) = F(k,n)) & (n > k implies (f . x) = ( 0. CNS())) by A5;

 hence (f . x) in the carrier of CNS();

 end;

 then

 reconsider f as sequence of CNS() by A4, FUNCT_2: 3;

 take seq = f;

 let n;

 n in NAT by ORDINAL1:def 12;

 then ex l be Nat st l = n & (l <= k implies (seq . n) = F(k,l)) & (l > k implies (seq . n) = ( 0. CNS())) by A5;

 hence thesis;

 end;

 definition

 let n, X, z, w;

 :: CLOPBAN4:def2

 func Expan (n,z,w) -> sequence of X means

 : Def2: for k be Nat holds (k <= n implies (it . k) = (((( Coef n) . k) * (z #N k)) * (w #N (n -' k)))) & (n < k implies (it . k) = ( 0. X));

 existence

 proof

 deffunc U( Nat, Nat) = (((( Coef $1) . $2) * (z #N $2)) * (w #N ($1 -' $2)));

 for n holds ex seq st for k holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = ( 0. X)) from ExNormSpaceCASE;

 hence thesis;

 end;

 uniqueness

 proof

 let seq1, seq2;

 assume that

 A1: for k holds (k <= n implies (seq1 . k) = (((( Coef n) . k) * (z #N k)) * (w #N (n -' k)))) & (k > n implies (seq1 . k) = ( 0. X)) and

 A2: for k holds (k <= n implies (seq2 . k) = (((( Coef n) . k) * (z #N k)) * (w #N (n -' k)))) & (k > n implies (seq2 . k) = ( 0. X));

 now

 let k be Element of NAT ;

 per cases ;

 suppose

 A3: k <= n;



 hence (seq1 . k) = (((( Coef n) . k) * (z #N k)) * (w #N (n -' k))) by A1

 .= (seq2 . k) by A2, A3;

 end;

 suppose

 A4: k > n;



 hence (seq1 . k) = ( 0. X) by A1

 .= (seq2 . k) by A2, A4;

 end;

 end;

 hence seq1 = seq2 by FUNCT_2: 63;

 end;

 end

 definition

 let n, X, z, w;

 :: CLOPBAN4:def3

 func Expan_e (n,z,w) -> sequence of X means

 : Def3: for k be Nat holds (k <= n implies (it . k) = (((( Coef_e n) . k) * (z #N k)) * (w #N (n -' k)))) & (n < k implies (it . k) = ( 0. X));

 existence

 proof

 deffunc U( Nat, Nat) = (((( Coef_e $1) . $2) * (z #N $2)) * (w #N ($1 -' $2)));

 for n holds ex seq st for k holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = ( 0. X)) from ExNormSpaceCASE;

 hence thesis;

 end;

 uniqueness

 proof

 let seq1, seq2;

 assume that

 A1: for k holds (k <= n implies (seq1 . k) = (((( Coef_e n) . k) * (z #N k)) * (w #N (n -' k)))) & (k > n implies (seq1 . k) = ( 0. X)) and

 A2: for k holds (k <= n implies (seq2 . k) = (((( Coef_e n) . k) * (z #N k)) * (w #N (n -' k)))) & (k > n implies (seq2 . k) = ( 0. X));

 now

 let k be Element of NAT ;

 per cases ;

 suppose

 A3: k <= n;



 hence (seq1 . k) = (((( Coef_e n) . k) * (z #N k)) * (w #N (n -' k))) by A1

 .= (seq2 . k) by A2, A3;

 end;

 suppose

 A4: k > n;



 hence (seq1 . k) = ( 0. X) by A1

 .= (seq2 . k) by A2, A4;

 end;

 end;

 hence seq1 = seq2 by FUNCT_2: 63;

 end;

 end

 definition

 let n, X, z, w;

 :: CLOPBAN4:def4

 func Alfa (n,z,w) -> sequence of X means

 : Def4: for k be Nat holds (k <= n implies (it . k) = (((z ExpSeq ) . k) * (( Partial_Sums (w ExpSeq )) . (n -' k)))) & (n < k implies (it . k) = ( 0. X));

 existence

 proof

 deffunc U( Nat, Nat) = (((z ExpSeq ) . $2) * (( Partial_Sums (w ExpSeq )) . ($1 -' $2)));

 for n holds ex seq st for k holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = ( 0. X)) from ExNormSpaceCASE;

 hence thesis;

 end;

 uniqueness

 proof

 let seq1, seq2;

 assume that

 A1: for k holds (k <= n implies (seq1 . k) = (((z ExpSeq ) . k) * (( Partial_Sums (w ExpSeq )) . (n -' k)))) & (k > n implies (seq1 . k) = ( 0. X)) and

 A2: for k holds (k <= n implies (seq2 . k) = (((z ExpSeq ) . k) * (( Partial_Sums (w ExpSeq )) . (n -' k)))) & (k > n implies (seq2 . k) = ( 0. X));

 now

 let k be Element of NAT ;

 per cases ;

 suppose

 A3: k <= n;



 hence (seq1 . k) = (((z ExpSeq ) . k) * (( Partial_Sums (w ExpSeq )) . (n -' k))) by A1

 .= (seq2 . k) by A2, A3;

 end;

 suppose

 A4: k > n;



 hence (seq1 . k) = ( 0. X) by A1

 .= (seq2 . k) by A2, A4;

 end;

 end;

 hence seq1 = seq2 by FUNCT_2: 63;

 end;

 end

 definition

 let X, z, w, n;

 :: CLOPBAN4:def5

 func Conj (n,z,w) -> sequence of X means

 : Def5: for k be Nat holds (k <= n implies (it . k) = (((z ExpSeq ) . k) * ((( Partial_Sums (w ExpSeq )) . n) - (( Partial_Sums (w ExpSeq )) . (n -' k))))) & (n < k implies (it . k) = ( 0. X));

 existence

 proof

 deffunc U( Nat, Nat) = (((z ExpSeq ) . $2) * ((( Partial_Sums (w ExpSeq )) . $1) - (( Partial_Sums (w ExpSeq )) . ($1 -' $2))));

 for n holds ex seq st for k holds (k <= n implies (seq . k) = U(n,k)) & (k > n implies (seq . k) = ( 0. X)) from ExNormSpaceCASE;

 hence thesis;

 end;

 uniqueness

 proof

 let seq1, seq2;

 assume that

 A1: for k holds (k <= n implies (seq1 . k) = (((z ExpSeq ) . k) * ((( Partial_Sums (w ExpSeq )) . n) - (( Partial_Sums (w ExpSeq )) . (n -' k))))) & (k > n implies (seq1 . k) = ( 0. X)) and

 A2: for k holds (k <= n implies (seq2 . k) = (((z ExpSeq ) . k) * ((( Partial_Sums (w ExpSeq )) . n) - (( Partial_Sums (w ExpSeq )) . (n -' k))))) & (k > n implies (seq2 . k) = ( 0. X));

 now

 let k be Element of NAT ;

 per cases ;

 suppose

 A3: k <= n;



 hence (seq1 . k) = (((z ExpSeq ) . k) * ((( Partial_Sums (w ExpSeq )) . n) - (( Partial_Sums (w ExpSeq )) . (n -' k)))) by A1

 .= (seq2 . k) by A2, A3;

 end;

 suppose

 A4: k > n;



 hence (seq1 . k) = ( 0. X) by A1

 .= (seq2 . k) by A2, A4;

 end;

 end;

 hence seq1 = seq2 by FUNCT_2: 63;

 end;

 end

 theorem :: CLOPBAN4:13



 Th13: ((z ExpSeq ) . (n + 1)) = ((( 1r / (n + 1)) * z) * ((z ExpSeq ) . n)) & ((z ExpSeq ) . 0 ) = ( 1. X) & ||.((z ExpSeq ) . n).|| <= (( ||.z.|| rExpSeq ) . n)

 proof

 defpred X[ Nat] means ||.((z ExpSeq ) . $1).|| <= (( ||.z.|| rExpSeq ) . $1);



 A1: ((z ExpSeq ) . 0 ) = (( 1r / ( 0 ! )) * (z #N 0 )) by Def1

 .= (( 1r / ( 0 ! )) * ((z GeoSeq ) . 0 )) by CLOPBAN3:def 8

 .= ( 1r * ( 1. X)) by CLOPBAN3:def 7, SIN_COS: 1

 .= ( 1. X) by CLVECT_1:def 5;

 A2:

 now

 let n be Nat;



 thus ((z ExpSeq ) . (n + 1)) = (( 1r / ((n + 1) ! )) * (z #N (n + 1))) by Def1

 .= (( 1r / ((n + 1) ! )) * ((z GeoSeq ) . (n + 1))) by CLOPBAN3:def 8

 .= (( 1r / ((n + 1) ! )) * (((z GeoSeq ) . n) * z)) by CLOPBAN3:def 7

 .= (( 1r / ((n + 1) ! )) * ((z #N n) * z)) by CLOPBAN3:def 8

 .= (( 1r / ((n ! ) * (n + 1))) * ((z #N n) * z)) by SIN_COS: 1

 .= ((( 1r * 1r ) / ((n ! ) * (n + 1))) * (z * (z #N n))) by Lm1, COMPLEX1:def 4

 .= ((( 1r / (n ! )) * ( 1r / (n + 1))) * (z * (z #N n))) by XCMPLX_1: 76

 .= ((( 1r / (n + 1)) * z) * (( 1r / (n ! )) * (z #N n))) by CLOPBAN3: 38

 .= ((( 1r / (n + 1)) * z) * ((z ExpSeq ) . n)) by Def1;

 end;



 A3: for n be Nat st X[n] holds X[(n + 1)]

 proof

 let n such that

 A4: X[n];

 0 <= ||.(( 1r / (n + 1)) * z).|| by CLVECT_1: 105;

 then

 A5: ( ||.(( 1r / (n + 1)) * z).|| * ||.((z ExpSeq ) . n).||) <= ( ||.(( 1r / (n + 1)) * z).|| * (( ||.z.|| rExpSeq ) . n)) by A4, XREAL_1: 64;



 A6: ||.((( 1r / (n + 1)) * z) * ((z ExpSeq ) . n)).|| <= ( ||.(( 1r / (n + 1)) * z).|| * ||.((z ExpSeq ) . n).||) by CLOPBAN3: 38;

 |.(n + 1).| = (n + 1) by ABSVALUE:def 1;

 then |.( 1r / (n + 1)).| = (1 / (n + 1)) by COMPLEX1: 48, COMPLEX1: 67;

 then

 A7: ||.(( 1r / (n + 1)) * z).|| = ((1 / (n + 1)) * ||.z.||) by CLVECT_1:def 13;



 A8: (((1 / (n + 1)) * ||.z.||) * (( ||.z.|| rExpSeq ) . n)) = ((1 / (n + 1)) * ((( ||.z.|| rExpSeq ) . n) * ||.z.||))

 .= ((1 / (n + 1)) * ((( ||.z.|| |^ n) / (n ! )) * ||.z.||)) by SIN_COS:def 5

 .= ((1 / (n + 1)) * ((( ||.z.|| |^ n) * ||.z.||) / (n ! ))) by XCMPLX_1: 74

 .= ((1 / (n + 1)) * (( ||.z.|| |^ (n + 1)) / (n ! ))) by NEWTON: 6

 .= (( ||.z.|| |^ (n + 1)) / ((n ! ) * (n + 1))) by XCMPLX_1: 103

 .= (( ||.z.|| |^ (n + 1)) / ((n + 1) ! )) by NEWTON: 15

 .= (( ||.z.|| rExpSeq ) . (n + 1)) by SIN_COS:def 5;

 ||.((z ExpSeq ) . (n + 1)).|| = ||.((( 1r / (n + 1)) * z) * ((z ExpSeq ) . n)).|| by A2;

 hence thesis by A6, A7, A5, A8, XXREAL_0: 2;

 end;

 (( ||.z.|| rExpSeq ) . 0 ) = (( ||.z.|| |^ 0 ) / ( 0 ! )) by SIN_COS:def 5

 .= (1 / ( 0 ! )) by NEWTON: 4

 .= (1 / ( Prod_real_n . 0 )) by SIN_COS:def 3

 .= (1 / 1) by SIN_COS:def 2

 .= 1;

 then

 A9: X[ 0 ] by A1, CLOPBAN3: 38;

 for n holds X[n] from NAT_1:sch 2( A9, A3);

 hence thesis by A2, A1;

 end;

 theorem :: CLOPBAN4:14

 0 < k implies (( Shift seq) . k) = (seq . (k -' 1)) by LOPBAN_4: 15;

 theorem :: CLOPBAN4:15



 Th15: (( Partial_Sums seq) . k) = ((( Partial_Sums ( Shift seq)) . k) + (seq . k))

 proof

 defpred X[ Nat] means (( Partial_Sums seq) . $1) = ((( Partial_Sums ( Shift seq)) . $1) + (seq . $1));



 A1: for k st X[k] holds X[(k + 1)]

 proof

 let k;

 assume (( Partial_Sums seq) . k) = ((( Partial_Sums ( Shift seq)) . k) + (seq . k));



 hence (( Partial_Sums seq) . (k + 1)) = (((( Partial_Sums ( Shift seq)) . k) + (seq . k)) + (seq . (k + 1))) by BHSP_4:def 1

 .= (((( Partial_Sums ( Shift seq)) . k) + (( Shift seq) . (k + 1))) + (seq . (k + 1))) by LOPBAN_4:def 5

 .= ((( Partial_Sums ( Shift seq)) . (k + 1)) + (seq . (k + 1))) by BHSP_4:def 1;

 end;

 (( Partial_Sums seq) . 0 ) = (seq . 0 ) by BHSP_4:def 1

 .= (( 0. X) + (seq . 0 )) by RLVECT_1: 4

 .= ((( Shift seq) . 0 ) + (seq . 0 )) by LOPBAN_4:def 5

 .= ((( Partial_Sums ( Shift seq)) . 0 ) + (seq . 0 )) by BHSP_4:def 1;

 then

 A2: X[ 0 ];

 for k holds X[k] from NAT_1:sch 2( A2, A1);

 hence thesis;

 end;

 theorem :: CLOPBAN4:16



 Th16: for z, w st (z,w) are_commutative holds ((z + w) #N n) = (( Partial_Sums ( Expan (n,z,w))) . n)

 proof

 let z, w such that

 A1: (z,w) are_commutative ;

 defpred X[ Nat] means ((z + w) #N $1) = (( Partial_Sums ( Expan ($1,z,w))) . $1);



 A2: for n st X[n] holds X[(n + 1)]

 proof

 let n such that

 A3: ((z + w) #N n) = (( Partial_Sums ( Expan (n,z,w))) . n);



 A4: n < (n + 1) by XREAL_1: 29;

 now

 let k be Element of NAT ;



 A5: n in NAT by ORDINAL1:def 12;

 A6:

 now

 A7:

 now

 assume

 A8: k < (n + 1);

 A9:

 now



 A10: ((k + 1) - 1) <= ((n + 1) - 1) by A8, A5, INT_1: 7;



 then

 A11: ((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

 A12: ((n ! ) / ((k ! ) * ((n -' k) ! ))) = (((n ! ) * ((n + 1) - k)) / (((k ! ) * ((n -' k) ! )) * (((n + 1) - k) + ( 0 * )))) by XCMPLX_1: 91

 .= (((n ! ) * ((n + 1) - k)) / ((k ! ) * (((n -' k) ! ) * (((n + 1) - k) + ( 0 * )))))

 .= (((n ! ) * ((n + 1) - k)) / ((k ! ) * (((n + 1) -' k) ! ))) by A10, SIN_COS: 2;

 assume

 A13: k <> 0 ;

 then

 A14: 0 < 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 A10, 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;

 ((((k -' 1) ! ) * ((n -' (k -' 1)) ! )) * k) = ((k * ((k -' 1) ! )) * ((n -' (k -' 1)) ! ))

 .= (((k + ( 0 * )) * ((k -' 1) ! )) * ((n -' (k -' 1)) ! ))

 .= ((k ! ) * (((n + 1) -' k) ! )) by A14, A18, SIN_COS: 2;

 then

 A19: ((n ! ) / (((k -' 1) ! ) * ((n -' (k -' 1)) ! ))) = (((n ! ) * k) / ((k ! ) * (((n + 1) -' k) ! ))) by A13, XCMPLX_1: 91;

 ((( Coef n) . k) + (( Coef n) . (k -' 1))) = (((n ! ) / ((k ! ) * ((n -' k) ! ))) + (( Coef n) . (k -' 1))) by A10, SIN_COS:def 6

 .= (((n ! ) / ((k ! ) * ((n -' k) ! ))) + ((n ! ) / (((k -' 1) ! ) * ((n -' (k -' 1)) ! )))) by A17, SIN_COS:def 6;



 then

 A20: ((( Coef n) . k) + (( Coef n) . (k -' 1))) = ((((n ! ) * ((n + 1) - k)) + ((n ! ) * k)) / ((k ! ) * (((n + 1) -' k) ! ))) by A12, A19, XCMPLX_1: 62

 .= (((n ! ) * (((n + 1) - k) + k)) / ((k ! ) * (((n + 1) -' k) ! )))

 .= (((n ! ) * ((((n + 1) - k) + k) + (( 0 + 0 ) * ))) / ((k ! ) * (((n + 1) -' k) ! )))

 .= (((n + 1) ! ) / ((k ! ) * (((n + 1) -' k) ! ))) by SIN_COS: 1

 .= (( Coef (n + 1)) . k) by A8, SIN_COS:def 6;



 A21: (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;

 (((( 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 A13, LOPBAN_4: 15

 .= (((( 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 A10, Def2

 .= (((((( 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, Def2

 .= ((((( 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 GROUP_1:def 3

 .= ((((( 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 GROUP_1:def 3

 .= ((((( 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 GROUP_1:def 3

 .= ((((( 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 CLOPBAN3: 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 (((( 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 A11, A21, A16, CLOPBAN3: 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 CLOPBAN3: 38

 .= (((( Coef n) . k) + (( Coef n) . (k -' 1))) * ((z #N k) * (w #N ((n + 1) -' k)))) by CLOPBAN3: 38;



 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 A20, CLOPBAN3: 38

 .= (( Expan ((n + 1),z,w)) . k) by A8, Def2;

 hence (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (( Expan ((n + 1),z,w)) . k);

 end;

 now



 A22: ((n + 1) -' 0 ) = ((n + 1) - 0 ) by XREAL_1: 233;



 then

 A23: (( Coef (n + 1)) . 0 ) = (((n + 1) ! ) / (1 * ((n + 1) ! ))) by SIN_COS: 1, SIN_COS:def 6

 .= 1 by XCMPLX_1: 60;



 A24: (n -' 0 ) = (n - 0 ) by XREAL_1: 233;



 then

 A25: (( Coef n) . 0 ) = ((n ! ) / (1 * (n ! ))) by SIN_COS: 1, SIN_COS:def 6

 .= 1 by XCMPLX_1: 60;

 assume

 A26: k = 0 ;



 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 LOPBAN_4:def 5

 .= ((( Expan (n,z,w)) . 0 ) * w) by RLVECT_1:def 4

 .= ((((( Coef n) . 0 ) * (z #N 0 )) * (w #N (n -' 0 ))) * w) by Def2

 .= (((( Coef n) . 0 ) * (z #N 0 )) * ((w #N (n -' 0 )) * w)) by GROUP_1:def 3

 .= (((( 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, Def2;

 hence (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (( Expan ((n + 1),z,w)) . k);

 end;

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

 end;

 A27:

 now



 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) ! ) * 1)) by SIN_COS: 1, SIN_COS:def 6

 .= 1 by XCMPLX_1: 60;



 A30: n < (n + 1) by XREAL_1: 29;



 A31: (n -' n) = (n - n) by XREAL_1: 233

 .= 0 ;



 then

 A32: (( Coef n) . n) = ((n ! ) / ((n ! ) * 1)) by SIN_COS: 1, SIN_COS:def 6

 .= 1 by XCMPLX_1: 60;

 assume

 A33: k = (n + 1);



 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 A30, Def2

 .= (( 0. X) + (( Shift (( Expan (n,z,w)) * z)) . (n + 1))) by CLOPBAN3: 38

 .= (( Shift (( Expan (n,z,w)) * z)) . (n + 1)) by RLVECT_1:def 4

 .= ((( Expan (n,z,w)) * z) . n) by LOPBAN_4:def 5

 .= ((( Expan (n,z,w)) . n) * z) by LOPBAN_3:def 6

 .= ((((( Coef n) . n) * (z #N n)) * (w #N (n -' n))) * z) by Def2

 .= (((( Coef n) . n) * (z #N n)) * ((w #N (n -' n)) * z)) by GROUP_1:def 3

 .= (((( 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 GROUP_1:def 3

 .= (((( Coef n) . n) * ((z #N n) * z)) * (w #N (n -' n))) by CLOPBAN3: 38

 .= (((( Coef (n + 1)) . (n + 1)) * (z #N (n + 1))) * (w #N (n -' n))) by A32, A29, Lm1

 .= (( Expan ((n + 1),z,w)) . k) by A33, A31, A28, Def2;

 hence (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (( Expan ((n + 1),z,w)) . k);

 end;

 assume k <= (n + 1);

 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;

 end;

 now

 assume

 A34: (n + 1) < 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 A34, LOPBAN_4: 15

 .= (((( 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, Def2

 .= (( 0. X) + ((( Expan (n,z,w)) . (k -' 1)) * z)) by CLOPBAN3: 38

 .= (( 0. X) + (( 0. X) * z)) by A35, A37, Def2

 .= (( 0. X) + ( 0. X)) by CLOPBAN3: 38

 .= ( 0. X) by RLVECT_1:def 4;

 hence (((( Expan (n,z,w)) * w) + ( Shift (( Expan (n,z,w)) * z))) . k) = (( Expan ((n + 1),z,w)) . k) by A34, Def2;

 end;

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

 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, Def2

 .= ((( Partial_Sums (( Expan (n,z,w)) * w)) . n) + ( 0. X)) by CLOPBAN3: 38

 .= (( Partial_Sums (( Expan (n,z,w)) * w)) . n) by RLVECT_1:def 4;

 (( 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, Def2

 .= ((( Partial_Sums (( Expan (n,z,w)) * z)) . n) + ( 0. X)) by CLOPBAN3: 38

 .= (( Partial_Sums (( Expan (n,z,w)) * z)) . n) by RLVECT_1:def 4;

 ( 0 + n) < (n + 1) by XREAL_1: 29;

 then

 A42: (( Expan (n,z,w)) . (n + 1)) = ( 0. X) by Def2;

 (( 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 Th15;



 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, CLOPBAN3: 38

 .= (( Partial_Sums ( Shift (( Expan (n,z,w)) * z))) . (n + 1)) by RLVECT_1:def 4;

 now

 let k be Element of NAT ;



 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 VECTSP_1:def 2

 .= (((( 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;

 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 + 1)) by CLOPBAN3:def 8

 .= ((((z + w) GeoSeq ) . n) * (z + w)) by CLOPBAN3:def 7

 .= ((( Partial_Sums ( Expan (n,z,w))) . n) * (z + w)) by A3, CLOPBAN3:def 8

 .= ((( Partial_Sums ( Expan (n,z,w))) * (z + w)) . n) by 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, CLOPBAN3: 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, CLOPBAN3: 15;

 end;



 A45: ((z + w) #N 0 ) = (((z + w) GeoSeq ) . 0 ) by CLOPBAN3:def 8

 .= ( 1. X) by CLOPBAN3:def 7;



 A46: ( 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 A46, Def2

 .= ((( 1r / ( 1r * 1r )) * (z #N 0 )) * (w #N 0 )) by A46, COMPLEX1:def 4, SIN_COS: 1, SIN_COS:def 6

 .= ((z #N 0 ) * (w #N 0 )) by CLVECT_1:def 5, COMPLEX1:def 4

 .= (((z GeoSeq ) . 0 ) * (w #N 0 )) by CLOPBAN3:def 8

 .= (((z GeoSeq ) . 0 ) * ((w GeoSeq ) . 0 )) by CLOPBAN3:def 8

 .= (( 1. X) * ((w GeoSeq ) . 0 )) by CLOPBAN3:def 7

 .= (( 1. X) * ( 1. X)) by CLOPBAN3:def 7

 .= ( 1. X) by VECTSP_1:def 4;

 then

 A47: X[ 0 ] by A45;

 for n holds X[n] from NAT_1:sch 2( A47, A2);

 hence thesis;

 end;

 theorem :: CLOPBAN4:17



 Th17: ( Expan_e (n,z,w)) = (( 1r / (n ! )) * ( Expan (n,z,w)))

 proof

 now

 let k be Element of NAT ;

 A1:

 now

 reconsider s = (n ! ) as Element of COMPLEX by XCMPLX_0:def 2;



 A2: ( 1r / ((k ! ) * ((n -' k) ! ))) = ((((n ! ) * 1r ) / (n ! )) / ((k ! ) * ((n -' k) ! ))) by COMPLEX1:def 4, XCMPLX_1: 60

 .= ((( 1r / (n ! )) * (n ! )) / ((k ! ) * ((n -' k) ! ))) by XCMPLX_1: 74;

 assume

 A3: k <= n;



 hence (( Expan_e (n,z,w)) . k) = (((( Coef_e n) . k) * (z #N k)) * (w #N (n -' k))) by Def3

 .= ((( 1r / ((k ! ) * ((n -' k) ! ))) * (z #N k)) * (w #N (n -' k))) by A3, SIN_COS:def 7;



 hence (( Expan_e (n,z,w)) . k) = (((( 1r / (n ! )) * (n ! )) / ((k ! ) * ((n -' k) ! ))) * ((z #N k) * (w #N (n -' k)))) by A2, CLOPBAN3: 38

 .= ((( 1r / (n ! )) * ((n ! ) / ((k ! ) * ((n -' k) ! )))) * ((z #N k) * (w #N (n -' k)))) by XCMPLX_1: 74

 .= (( 1r / s) * ((s / ((k ! ) * ((n -' k) ! ))) * ((z #N k) * (w #N (n -' k))))) by CLOPBAN3: 38

 .= (( 1r / s) * (((s / ((k ! ) * ((n -' k) ! ))) * (z #N k)) * (w #N (n -' k)))) by CLOPBAN3: 38

 .= (( 1r / (n ! )) * (((( Coef n) . k) * (z #N k)) * (w #N (n -' k)))) by A3, SIN_COS:def 6

 .= (( 1r / (n ! )) * (( Expan (n,z,w)) . k)) by A3, Def2

 .= ((( 1r / (n ! )) * ( Expan (n,z,w))) . k) by CLVECT_1:def 14;

 end;

 now

 assume

 A4: n < k;



 hence (( Expan_e (n,z,w)) . k) = ( 0. X) by Def3

 .= (( 1r / (n ! )) * ( 0. X)) by CLVECT_1: 1

 .= (( 1r / (n ! )) * (( Expan (n,z,w)) . k)) by A4, Def2

 .= ((( 1r / (n ! )) * ( Expan (n,z,w))) . k) by CLVECT_1:def 14;

 end;

 hence (( Expan_e (n,z,w)) . k) = ((( 1r / (n ! )) * ( Expan (n,z,w))) . k) by A1;

 end;

 hence thesis by FUNCT_2: 63;

 end;

 theorem :: CLOPBAN4:18



 Th18: for z, w st (z,w) are_commutative holds (( 1r / (n ! )) * ((z + w) #N n)) = (( Partial_Sums ( Expan_e (n,z,w))) . n)

 proof

 let z, w;

 assume (z,w) are_commutative ;



 hence (( 1r / (n ! )) * ((z + w) #N n)) = (( 1r / (n ! )) * (( Partial_Sums ( Expan (n,z,w))) . n)) by Th16

 .= ((( 1r / (n ! )) * ( Partial_Sums ( Expan (n,z,w)))) . n) by CLVECT_1:def 14

 .= (( Partial_Sums (( 1r / (n ! )) * ( Expan (n,z,w)))) . n) by CLOPBAN3: 19

 .= (( Partial_Sums ( Expan_e (n,z,w))) . n) by Th17;

 end;

 theorem :: CLOPBAN4:19



 Th19: (( 0. X) ExpSeq ) is norm_summable & ( Sum (( 0. X) ExpSeq )) = ( 1. X)

 proof

 reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

 defpred X[ set] means (( Partial_Sums ||.(( 0. X) ExpSeq ).||) . $1) = jj;



 A1: for n be Nat st X[n] holds X[(n + 1)]

 proof

 let n be Nat such that

 A2: (( Partial_Sums ||.(( 0. X) ExpSeq ).||) . n) = jj;



 thus (( Partial_Sums ||.(( 0. X) ExpSeq ).||) . (n + 1)) = (1 + ( ||.(( 0. X) ExpSeq ).|| . (n + 1))) by A2, SERIES_1:def 1

 .= (1 + ||.((( 0. X) ExpSeq ) . (n + 1)).||) by NORMSP_0:def 4

 .= (1 + ||.((( 1r / (n + 1)) * ( 0. X)) * ((( 0. X) ExpSeq ) . n)).||) by Th13

 .= (1 + ||.(( 0. X) * ((( 0. X) ExpSeq ) . n)).||) by CLVECT_1: 1

 .= (1 + ||.( 0. X).||) by CLOPBAN3: 38

 .= (1 + 0 ) by CLOPBAN3: 38

 .= jj;

 end;

 (( Partial_Sums ||.(( 0. X) ExpSeq ).||) . 0 ) = ( ||.(( 0. X) ExpSeq ).|| . 0 ) by SERIES_1:def 1

 .= ||.((( 0. X) ExpSeq ) . 0 ).|| by NORMSP_0:def 4

 .= ||.( 1. X).|| by Th13

 .= 1 by CLOPBAN3: 38;

 then

 A3: X[ 0 ];

 for n be Nat holds X[n] from NAT_1:sch 2( A3, A1);

 then ( Partial_Sums ||.(( 0. X) ExpSeq ).||) is constant by VALUED_0:def 18;

 then

 A4: ||.(( 0. X) ExpSeq ).|| is summable by SERIES_1:def 2;

 defpred X[ set] means (( Partial_Sums (( 0. X) ExpSeq )) . $1) = ( 1. X);



 A5: for n st X[n] holds X[(n + 1)]

 proof

 let n;

 assume (( Partial_Sums (( 0. X) ExpSeq )) . n) = ( 1. X);



 hence (( Partial_Sums (( 0. X) ExpSeq )) . (n + 1)) = (( 1. X) + ((( 0. X) ExpSeq ) . (n + 1))) by BHSP_4:def 1

 .= (( 1. X) + ((( 1r / (n + 1)) * ( 0. X)) * ((( 0. X) ExpSeq ) . n))) by Th13

 .= (( 1. X) + (( 0. X) * ((( 0. X) ExpSeq ) . n))) by CLVECT_1: 1

 .= (( 1. X) + ( 0. X)) by CLOPBAN3: 38

 .= ( 1. X) by RLVECT_1:def 4;

 end;

 (( Partial_Sums (( 0. X) ExpSeq )) . 0 ) = ((( 0. X) ExpSeq ) . 0 ) by BHSP_4:def 1

 .= ( 1. X) by Th13;

 then

 A6: X[ 0 ];

 for n holds X[n] from NAT_1:sch 2( A6, A5);

 then ( lim ( Partial_Sums (( 0. X) ExpSeq ))) = ( 1. X) by Th2;

 hence thesis by A4, CLOPBAN3:def 2, CLOPBAN3:def 3;

 end;

 registration

 let X;

 let z be Element of X;

 cluster (z ExpSeq ) -> norm_summable;

 coherence

 proof

 ex m be Nat st for n be Nat st m <= n holds ||.((z ExpSeq ) . n).|| <= (( ||.z.|| rExpSeq ) . n)

 proof

 take 0 ;

 thus thesis by Th13;

 end;

 hence thesis by CLOPBAN3: 27, SIN_COS: 45;

 end;

 end

 theorem :: CLOPBAN4:20



 Th20: ((z ExpSeq ) . 0 ) = ( 1. X) & (( Expan ( 0 ,z,w)) . 0 ) = ( 1. X)

 proof



 thus ((z ExpSeq ) . 0 ) = (( 1r / ( 0 ! )) * (z #N 0 )) by Def1

 .= (( 1r / ( 0 ! )) * ((z GeoSeq ) . 0 )) by CLOPBAN3:def 8

 .= ( 1r * ( 1. X)) by CLOPBAN3:def 7, SIN_COS: 1

 .= ( 1. X) by CLVECT_1:def 5;



 A1: ( 0 -' 0 ) = 0 by XREAL_1: 232;



 hence (( Expan ( 0 ,z,w)) . 0 ) = (((( Coef 0 ) . 0 ) * (z #N 0 )) * (w #N 0 )) by Def2

 .= ((( 1r / ( 1r * 1r )) * (z #N 0 )) * (w #N 0 )) by A1, COMPLEX1:def 4, SIN_COS: 1, SIN_COS:def 6

 .= ((z #N 0 ) * (w #N 0 )) by CLVECT_1:def 5, COMPLEX1:def 4

 .= (((z GeoSeq ) . 0 ) * (w #N 0 )) by CLOPBAN3:def 8

 .= (((z GeoSeq ) . 0 ) * ((w GeoSeq ) . 0 )) by CLOPBAN3:def 8

 .= (( 1. X) * ((w GeoSeq ) . 0 )) by CLOPBAN3:def 7

 .= (( 1. X) * ( 1. X)) by CLOPBAN3:def 7

 .= ( 1. X) by VECTSP_1:def 4;

 end;

 theorem :: CLOPBAN4:21



 Th21: l <= k implies (( Alfa ((k + 1),z,w)) . l) = ((( Alfa (k,z,w)) . l) + (( Expan_e ((k + 1),z,w)) . l))

 proof

 assume

 A1: l <= k;



 A2: k < (k + 1) by XREAL_1: 29;

 then

 A3: l <= (k + 1) by A1, XXREAL_0: 2;



 A4: (((z ExpSeq ) . l) * ((w ExpSeq ) . ((k + 1) -' l))) = ((( 1r / (l ! )) * (z #N l)) * ((w ExpSeq ) . ((k + 1) -' l))) by Def1

 .= ((( 1r / (l ! )) * (z #N l)) * (( 1r / (((k + 1) -' l) ! )) * (w #N ((k + 1) -' l)))) by Def1

 .= ((( 1r / (l ! )) * ( 1r / (((k + 1) -' l) ! ))) * ((z #N l) * (w #N ((k + 1) -' l)))) by CLOPBAN3: 38

 .= ((( 1r * 1r ) / ((l ! ) * (((k + 1) -' l) ! ))) * ((z #N l) * (w #N ((k + 1) -' l)))) by XCMPLX_1: 76

 .= ((( Coef_e (k + 1)) . l) * ((z #N l) * (w #N ((k + 1) -' l)))) by A3, COMPLEX1:def 4, SIN_COS:def 7

 .= (((( Coef_e (k + 1)) . l) * (z #N l)) * (w #N ((k + 1) -' l))) by CLOPBAN3: 38

 .= (( Expan_e ((k + 1),z,w)) . l) by A3, Def3;

 ((k + 1) -' l) = ((k + 1) - l) by A1, A2, XREAL_1: 233, XXREAL_0: 2;



 then

 A5: ((k + 1) -' l) = ((k - l) + 1)

 .= ((k -' l) + 1) by A1, XREAL_1: 233;



 then (( Alfa ((k + 1),z,w)) . l) = (((z ExpSeq ) . l) * (( Partial_Sums (w ExpSeq )) . ((k -' l) + 1))) by A3, Def4

 .= (((z ExpSeq ) . l) * ((( Partial_Sums (w ExpSeq )) . (k -' l)) + ((w ExpSeq ) . ((k + 1) -' l)))) by A5, BHSP_4:def 1

 .= ((((z ExpSeq ) . l) * (( Partial_Sums (w ExpSeq )) . (k -' l))) + (((z ExpSeq ) . l) * ((w ExpSeq ) . ((k + 1) -' l)))) by VECTSP_1:def 2

 .= ((( Alfa (k,z,w)) . l) + (((z ExpSeq ) . l) * ((w ExpSeq ) . ((k + 1) -' l)))) by A1, Def4;

 hence thesis by A4;

 end;

 theorem :: CLOPBAN4:22



 Th22: (( Partial_Sums ( Alfa ((k + 1),z,w))) . k) = ((( Partial_Sums ( Alfa (k,z,w))) . k) + (( Partial_Sums ( Expan_e ((k + 1),z,w))) . k))

 proof

 now

 let l be Nat;

 assume l <= k;



 hence (( Alfa ((k + 1),z,w)) . l) = ((( Alfa (k,z,w)) . l) + (( Expan_e ((k + 1),z,w)) . l)) by Th21

 .= ((( Alfa (k,z,w)) + ( Expan_e ((k + 1),z,w))) . l) by NORMSP_1:def 2;

 end;



 hence (( Partial_Sums ( Alfa ((k + 1),z,w))) . k) = (( Partial_Sums (( Alfa (k,z,w)) + ( Expan_e ((k + 1),z,w)))) . k) by Th11

 .= ((( Partial_Sums ( Alfa (k,z,w))) + ( Partial_Sums ( Expan_e ((k + 1),z,w)))) . k) by CLOPBAN3: 15

 .= ((( Partial_Sums ( Alfa (k,z,w))) . k) + (( Partial_Sums ( Expan_e ((k + 1),z,w))) . k)) by NORMSP_1:def 2;

 end;

 theorem :: CLOPBAN4:23



 Th23: ((z ExpSeq ) . k) = (( Expan_e (k,z,w)) . k)

 proof

 0 = (k - k);

 then

 A1: (k -' k) = 0 by XREAL_1: 233;



 hence (( Expan_e (k,z,w)) . k) = (((( Coef_e k) . k) * (z #N k)) * (w #N 0 )) by Def3

 .= (((( Coef_e k) . k) * (z #N k)) * ( 1. X)) by CLOPBAN3: 39

 .= ((( Coef_e k) . k) * (z #N k)) by VECTSP_1:def 4

 .= (( 1r / ((k ! ) * 1r )) * (z #N k)) by A1, COMPLEX1:def 4, SIN_COS: 1, SIN_COS:def 7

 .= ((z ExpSeq ) . k) by Def1, COMPLEX1:def 4;

 end;

 theorem :: CLOPBAN4:24



 Th24: for z, w st (z,w) are_commutative holds (( Partial_Sums ((z + w) ExpSeq )) . n) = (( Partial_Sums ( Alfa (n,z,w))) . n)

 proof

 let z, w such that

 A1: (z,w) are_commutative ;

 defpred X[ Nat] means (( Partial_Sums ((z + w) ExpSeq )) . $1) = (( Partial_Sums ( Alfa ($1,z,w))) . $1);



 A2: for k st X[k] holds X[(k + 1)]

 proof

 let k such that

 A3: (( Partial_Sums ((z + w) ExpSeq )) . k) = (( Partial_Sums ( Alfa (k,z,w))) . k);

 ((k + 1) -' (k + 1)) = 0 by XREAL_1: 232;



 then (( Alfa ((k + 1),z,w)) . (k + 1)) = (((z ExpSeq ) . (k + 1)) * (( Partial_Sums (w ExpSeq )) . 0 )) by Def4

 .= (((z ExpSeq ) . (k + 1)) * ((w ExpSeq ) . 0 )) by BHSP_4:def 1

 .= (((z ExpSeq ) . (k + 1)) * ( 1. X)) by Th20

 .= ((z ExpSeq ) . (k + 1)) by VECTSP_1:def 4

 .= (( Expan_e ((k + 1),z,w)) . (k + 1)) by Th23;



 then

 A4: ((( Partial_Sums ( Expan_e ((k + 1),z,w))) . k) + (( Alfa ((k + 1),z,w)) . (k + 1))) = (( Partial_Sums ( Expan_e ((k + 1),z,w))) . (k + 1)) by BHSP_4:def 1

 .= (( 1r / ((k + 1) ! )) * ((z + w) #N (k + 1))) by A1, Th18;

 (( Partial_Sums ( Alfa ((k + 1),z,w))) . (k + 1)) = ((( Partial_Sums ( Alfa ((k + 1),z,w))) . k) + (( Alfa ((k + 1),z,w)) . (k + 1))) by BHSP_4:def 1

 .= (((( Partial_Sums ( Alfa (k,z,w))) . k) + (( Partial_Sums ( Expan_e ((k + 1),z,w))) . k)) + (( Alfa ((k + 1),z,w)) . (k + 1))) by Th22

 .= ((( Partial_Sums ((z + w) ExpSeq )) . k) + ((( Partial_Sums ( Expan_e ((k + 1),z,w))) . k) + (( Alfa ((k + 1),z,w)) . (k + 1)))) by A3, RLVECT_1:def 3;



 then (( Partial_Sums ( Alfa ((k + 1),z,w))) . (k + 1)) = ((( Partial_Sums ((z + w) ExpSeq )) . k) + (((z + w) ExpSeq ) . (k + 1))) by A4, Def1

 .= (( Partial_Sums ((z + w) ExpSeq )) . (k + 1)) by BHSP_4:def 1;

 hence (( Partial_Sums ((z + w) ExpSeq )) . (k + 1)) = (( Partial_Sums ( Alfa ((k + 1),z,w))) . (k + 1));

 end;



 A5: (( Partial_Sums ((z + w) ExpSeq )) . 0 ) = (((z + w) ExpSeq ) . 0 ) by BHSP_4:def 1

 .= ( 1. X) by Th20;



 A6: ( 0 -' 0 ) = 0 by XREAL_1: 232;

 (( Partial_Sums ( Alfa ( 0 ,z,w))) . 0 ) = (( Alfa ( 0 ,z,w)) . 0 ) by BHSP_4:def 1

 .= (((z ExpSeq ) . 0 ) * (( Partial_Sums (w ExpSeq )) . 0 )) by A6, Def4

 .= (((z ExpSeq ) . 0 ) * ((w ExpSeq ) . 0 )) by BHSP_4:def 1

 .= (( 1. X) * ((w ExpSeq ) . 0 )) by Th20

 .= (( 1. X) * ( 1. X)) by Th20

 .= ( 1. X) by VECTSP_1:def 4;

 then

 A7: X[ 0 ] by A5;

 for n holds X[n] from NAT_1:sch 2( A7, A2);

 hence thesis;

 end;

 theorem :: CLOPBAN4:25



 Th25: for z, w st (z,w) are_commutative holds (((( Partial_Sums (z ExpSeq )) . k) * (( Partial_Sums (w ExpSeq )) . k)) - (( Partial_Sums ((z + w) ExpSeq )) . k)) = (( Partial_Sums ( Conj (k,z,w))) . k)

 proof

 let z, w;

 assume (z,w) are_commutative ;



 then

 A1: (((( Partial_Sums (z ExpSeq )) . k) * (( Partial_Sums (w ExpSeq )) . k)) - (( Partial_Sums ((z + w) ExpSeq )) . k)) = (((( Partial_Sums (z ExpSeq )) . k) * (( Partial_Sums (w ExpSeq )) . k)) - (( Partial_Sums ( Alfa (k,z,w))) . k)) by Th24

 .= (((( Partial_Sums (z ExpSeq )) * (( Partial_Sums (w ExpSeq )) . k)) . k) - (( Partial_Sums ( Alfa (k,z,w))) . k)) by LOPBAN_3:def 6

 .= ((( Partial_Sums ((z ExpSeq ) * (( Partial_Sums (w ExpSeq )) . k))) . k) - (( Partial_Sums ( Alfa (k,z,w))) . k)) by Th9

 .= ((( Partial_Sums ((z ExpSeq ) * (( Partial_Sums (w ExpSeq )) . k))) - ( Partial_Sums ( Alfa (k,z,w)))) . k) by NORMSP_1:def 3

 .= (( Partial_Sums (((z ExpSeq ) * (( Partial_Sums (w ExpSeq )) . k)) - ( Alfa (k,z,w)))) . k) by CLOPBAN3: 16;

 for l be Nat st l <= k holds ((((z ExpSeq ) * (( Partial_Sums (w ExpSeq )) . k)) - ( Alfa (k,z,w))) . l) = (( Conj (k,z,w)) . l)

 proof

 let l be Nat such that

 A2: l <= k;



 thus ((((z ExpSeq ) * (( Partial_Sums (w ExpSeq )) . k)) - ( Alfa (k,z,w))) . l) = ((((z ExpSeq ) * (( Partial_Sums (w ExpSeq )) . k)) . l) - (( Alfa (k,z,w)) . l)) by NORMSP_1:def 3

 .= ((((z ExpSeq ) . l) * (( Partial_Sums (w ExpSeq )) . k)) - (( Alfa (k,z,w)) . l)) by LOPBAN_3:def 6

 .= ((((z ExpSeq ) . l) * (( Partial_Sums (w ExpSeq )) . k)) - (((z ExpSeq ) . l) * (( Partial_Sums (w ExpSeq )) . (k -' l)))) by A2, Def4

 .= (((z ExpSeq ) . l) * ((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l)))) by CLOPBAN3: 38

 .= (( Conj (k,z,w)) . l) by A2, Def5;

 end;

 hence thesis by A1, Th11;

 end;

 theorem :: CLOPBAN4:26



 Th26: 0 <= (( ||.z.|| rExpSeq ) . n)

 proof

 defpred P[ Nat] means 0 <= ( ||.z.|| |^ $1);



 A1: for k st P[k] holds P[(k + 1)]

 proof

 let k such that

 A2: P[k];



 A3: 0 <= ||.z.|| by CLVECT_1: 105;

 ( ||.z.|| |^ (k + 1)) = (( ||.z.|| |^ k) * ||.z.||) by NEWTON: 6;

 hence thesis by A2, A3;

 end;



 A4: P[ 0 ] by NEWTON: 4;

 for k holds P[k] from NAT_1:sch 2( A4, A1);

 then

 A5: 0 <= ( ||.z.|| |^ n);



 A6: (( ||.z.|| |^ n) / (n ! )) = (( ||.z.|| |^ n) * ((n ! ) " )) by XCMPLX_0:def 9;

 thus thesis by A5, A6, SIN_COS:def 5;

 end;

 theorem :: CLOPBAN4:27



 Th27: ||.(( Partial_Sums (z ExpSeq )) . k).|| <= (( Partial_Sums ( ||.z.|| rExpSeq )) . k) & (( Partial_Sums ( ||.z.|| rExpSeq )) . k) <= ( Sum ( ||.z.|| rExpSeq )) & ||.(( Partial_Sums (z ExpSeq )) . k).|| <= ( Sum ( ||.z.|| rExpSeq ))

 proof

 defpred X[ Nat] means ||.(( Partial_Sums (z ExpSeq )) . $1).|| <= (( Partial_Sums ( ||.z.|| rExpSeq )) . $1);



 A1: (( Partial_Sums ( ||.z.|| rExpSeq )) . 0 ) = (( ||.z.|| rExpSeq ) . 0 ) by SERIES_1:def 1

 .= (( ||.z.|| |^ 0 ) / ( 0 ! )) by SIN_COS:def 5

 .= 1 by NEWTON: 4, NEWTON: 12;



 A2: for k st X[k] holds X[(k + 1)]

 proof

 let k;

 assume ||.(( Partial_Sums (z ExpSeq )) . k).|| <= (( Partial_Sums ( ||.z.|| rExpSeq )) . k);

 then

 A3: ( ||.(( Partial_Sums (z ExpSeq )) . k).|| + (( ||.z.|| rExpSeq ) . (k + 1))) <= ((( Partial_Sums ( ||.z.|| rExpSeq )) . k) + (( ||.z.|| rExpSeq ) . (k + 1))) by XREAL_1: 6;



 A4: ||.((( Partial_Sums (z ExpSeq )) . k) + ((z ExpSeq ) . (k + 1))).|| <= ( ||.(( Partial_Sums (z ExpSeq )) . k).|| + ||.((z ExpSeq ) . (k + 1)).||) by CLOPBAN3: 38;

 ||.((z ExpSeq ) . (k + 1)).|| <= (( ||.z.|| rExpSeq ) . (k + 1)) by Th13;

 then

 A5: ( ||.(( Partial_Sums (z ExpSeq )) . k).|| + ||.((z ExpSeq ) . (k + 1)).||) <= ( ||.(( Partial_Sums (z ExpSeq )) . k).|| + (( ||.z.|| rExpSeq ) . (k + 1))) by XREAL_1: 7;



 A6: ((( Partial_Sums ( ||.z.|| rExpSeq )) . k) + (( ||.z.|| rExpSeq ) . (k + 1))) = (( Partial_Sums ( ||.z.|| rExpSeq )) . (k + 1)) by SERIES_1:def 1;

 ||.(( Partial_Sums (z ExpSeq )) . (k + 1)).|| = ||.((( Partial_Sums (z ExpSeq )) . k) + ((z ExpSeq ) . (k + 1))).|| by BHSP_4:def 1;

 then ||.(( Partial_Sums (z ExpSeq )) . (k + 1)).|| <= ( ||.(( Partial_Sums (z ExpSeq )) . k).|| + (( ||.z.|| rExpSeq ) . (k + 1))) by A4, A5, XXREAL_0: 2;

 hence thesis by A3, A6, XXREAL_0: 2;

 end;

 ||.(( Partial_Sums (z ExpSeq )) . 0 ).|| = ||.((z ExpSeq ) . 0 ).|| by BHSP_4:def 1

 .= ||.(( 1r / ( 0 ! )) * (z #N 0 )).|| by Def1

 .= ||.(( 1r / ( 0 ! )) * ((z GeoSeq ) . 0 )).|| by CLOPBAN3:def 8

 .= ||.( 1r * ( 1. X)).|| by CLOPBAN3:def 7, SIN_COS: 1

 .= ||.( 1. X).|| by CLVECT_1:def 5

 .= 1 by CLOPBAN3: 38;

 then

 A7: X[ 0 ] by A1;



 A8: for k holds X[k] from NAT_1:sch 2( A7, A2);

 hence ||.(( Partial_Sums (z ExpSeq )) . k).|| <= (( Partial_Sums ( ||.z.|| rExpSeq )) . k);



 A9: for n holds 0 <= (( ||.z.|| rExpSeq ) . n) by Th26;

 ( ||.z.|| rExpSeq ) is summable by SIN_COS: 45;

 then

 A10: ( Partial_Sums ( ||.z.|| rExpSeq )) is bounded_above by A9, SERIES_1: 17;

 then (( Partial_Sums ( ||.z.|| rExpSeq )) . k) <= ( lim ( Partial_Sums ( ||.z.|| rExpSeq ))) by A9, SEQ_4: 37, SERIES_1: 16;

 hence (( Partial_Sums ( ||.z.|| rExpSeq )) . k) <= ( Sum ( ||.z.|| rExpSeq )) by SERIES_1:def 3;

 now

 let k;

 ( lim ( Partial_Sums ( ||.z.|| rExpSeq ))) = ( Sum ( ||.z.|| rExpSeq )) by SERIES_1:def 3;

 hence (( Partial_Sums ( ||.z.|| rExpSeq )) . k) <= ( Sum ( ||.z.|| rExpSeq )) by A9, A10, SEQ_4: 37, SERIES_1: 16;

 end;

 then

 A11: (( Partial_Sums ( ||.z.|| rExpSeq )) . k) <= ( Sum ( ||.z.|| rExpSeq ));

 ||.(( Partial_Sums (z ExpSeq )) . k).|| <= (( Partial_Sums ( ||.z.|| rExpSeq )) . k) by A8;

 hence thesis by A11, XXREAL_0: 2;

 end;

 theorem :: CLOPBAN4:28



 Th28: 1 <= ( Sum ( ||.z.|| rExpSeq ))

 proof

 ||.(( Partial_Sums (z ExpSeq )) . 0 ).|| = ||.((z ExpSeq ) . 0 ).|| by BHSP_4:def 1

 .= ||.( 1. X).|| by Th13

 .= 1 by CLOPBAN3: 38;

 hence thesis by Th27;

 end;

 theorem :: CLOPBAN4:29



 Th29: |.(( Partial_Sums ( ||.z.|| rExpSeq )) . n).| = (( Partial_Sums ( ||.z.|| rExpSeq )) . n) & (n <= m implies |.((( Partial_Sums ( ||.z.|| rExpSeq )) . m) - (( Partial_Sums ( ||.z.|| rExpSeq )) . n)).| = ((( Partial_Sums ( ||.z.|| rExpSeq )) . m) - (( Partial_Sums ( ||.z.|| rExpSeq )) . n)))

 proof

 for n holds 0 <= (( ||.z.|| rExpSeq ) . n) by Th26;

 hence thesis by COMSEQ_3: 9;

 end;

 theorem :: CLOPBAN4:30



 Th30: |.(( Partial_Sums ||.( Conj (k,z,w)).||) . n).| = (( Partial_Sums ||.( Conj (k,z,w)).||) . n)

 proof

 A1:

 now

 let n;

 ( ||.( Conj (k,z,w)).|| . n) = ||.(( Conj (k,z,w)) . n).|| by NORMSP_0:def 4;

 hence 0 <= ( ||.( Conj (k,z,w)).|| . n) by CLVECT_1: 105;

 end;

 then ( Partial_Sums ||.( Conj (k,z,w)).||) is non-decreasing by SERIES_1: 16;

 then

 A2: (( Partial_Sums ||.( Conj (k,z,w)).||) . 0 ) <= (( Partial_Sums ||.( Conj (k,z,w)).||) . n) by SEQM_3: 6;



 A3: (( Partial_Sums ||.( Conj (k,z,w)).||) . 0 ) = ( ||.( Conj (k,z,w)).|| . 0 ) by SERIES_1:def 1;

 0 <= ( ||.( Conj (k,z,w)).|| . 0 ) by A1;

 hence thesis by A2, A3, ABSVALUE:def 1;

 end;

 theorem :: CLOPBAN4:31



 Th31: for p be Real st p > 0 holds ex n st for k st n <= k holds |.(( Partial_Sums ||.( Conj (k,z,w)).||) . k).| 0 ;

 reconsider pp = p as Real;

 set p1 = ( min ((pp / (4 * ( Sum ( ||.z.|| rExpSeq )))),(pp / (4 * ( Sum ( ||.w.|| rExpSeq ))))));



 A2: 1 <= ( Sum ( ||.w.|| rExpSeq )) by Th28;



 A3: 1 <= ( Sum ( ||.z.|| rExpSeq )) by Th28;

 then

 A4: p1 > 0 by A1, A2, XXREAL_0: 15;

 ( Partial_Sums (w ExpSeq )) is convergent by CLOPBAN3:def 1;

 then for s be Real st 0 < s holds ex n be Nat st for m be Nat st n <= m holds ||.((( Partial_Sums (w ExpSeq )) . m) - (( Partial_Sums (w ExpSeq )) . n)).|| < s by CLOPBAN3: 4;

 then ( Partial_Sums (w ExpSeq )) is Cauchy_sequence_by_Norm by CLOPBAN3: 5;

 then

 consider n2 such that

 A5: for k,l be Nat st n2 <= k & n2 <= l holds ||.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . l)).|| < p1 by A4, CSSPACE3: 8;

 ( ||.z.|| rExpSeq ) is summable by SIN_COS: 45;

 then ( Partial_Sums ( ||.z.|| rExpSeq )) is convergent by SERIES_1:def 2;

 then

 consider n1 such that

 A6: for k,l be Nat st n1 <= k & n1 <= l holds |.((( Partial_Sums ( ||.z.|| rExpSeq )) . k) - (( Partial_Sums ( ||.z.|| rExpSeq )) . l)).| < p1 by A4, COMSEQ_3: 4;

 set n3 = (n1 + n2);

 take n4 = (n3 + n3);

 A7:

 now

 let n;

 let k;

 now

 let l be Nat such that

 A8: l <= k;



 A9: ||.(((z ExpSeq ) . l) * ((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l)))).|| <= ( ||.((z ExpSeq ) . l).|| * ||.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).||) by CLOPBAN3: 38;

 0 <= ||.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).|| by CLVECT_1: 105;

 then

 A10: ( ||.((z ExpSeq ) . l).|| * ||.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).||) <= ((( ||.z.|| rExpSeq ) . l) * ||.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).||) by Th13, XREAL_1: 64;

 ( ||.( Conj (k,z,w)).|| . l) = ||.(( Conj (k,z,w)) . l).|| by NORMSP_0:def 4

 .= ||.(((z ExpSeq ) . l) * ((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l)))).|| by A8, Def5;

 hence ( ||.( Conj (k,z,w)).|| . l) <= ((( ||.z.|| rExpSeq ) . l) * ||.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).||) by A9, A10, XXREAL_0: 2;

 end;

 hence for l be Nat st l <= k holds ( ||.( Conj (k,z,w)).|| . l) <= ((( ||.z.|| rExpSeq ) . l) * ||.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).||);

 end;

 A11:

 now

 let k;

 now

 let l be Nat;



 A12: ||.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).|| <= ( ||.(( Partial_Sums (w ExpSeq )) . k).|| + ||.(( Partial_Sums (w ExpSeq )) . (k -' l)).||) by CLVECT_1: 104;

 ||.(( Partial_Sums (w ExpSeq )) . (k -' l)).|| <= ( Sum ( ||.w.|| rExpSeq )) by Th27;

 then

 A13: (( Sum ( ||.w.|| rExpSeq )) + ||.(( Partial_Sums (w ExpSeq )) . (k -' l)).||) <= (( Sum ( ||.w.|| rExpSeq )) + ( Sum ( ||.w.|| rExpSeq ))) by XREAL_1: 6;

 ||.(( Partial_Sums (w ExpSeq )) . k).|| <= ( Sum ( ||.w.|| rExpSeq )) by Th27;

 then ( ||.(( Partial_Sums (w ExpSeq )) . k).|| + ||.(( Partial_Sums (w ExpSeq )) . (k -' l)).||) <= (( Sum ( ||.w.|| rExpSeq )) + ||.(( Partial_Sums (w ExpSeq )) . (k -' l)).||) by XREAL_1: 6;

 then ( ||.(( Partial_Sums (w ExpSeq )) . k).|| + ||.(( Partial_Sums (w ExpSeq )) . (k -' l)).||) <= (2 * ( Sum ( ||.w.|| rExpSeq ))) by A13, XXREAL_0: 2;

 then

 A14: ||.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).|| <= (2 * ( Sum ( ||.w.|| rExpSeq ))) by A12, XXREAL_0: 2;

 assume l <= k;

 then

 A15: ( ||.( Conj (k,z,w)).|| . l) <= ((( ||.z.|| rExpSeq ) . l) * ||.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).||) by A7;

 0 <= (( ||.z.|| rExpSeq ) . l) by Th26;

 then ((( ||.z.|| rExpSeq ) . l) * ||.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).||) <= ((( ||.z.|| rExpSeq ) . l) * (2 * ( Sum ( ||.w.|| rExpSeq )))) by A14, XREAL_1: 64;

 hence ( ||.( Conj (k,z,w)).|| . l) <= ((( ||.z.|| rExpSeq ) . l) * (2 * ( Sum ( ||.w.|| rExpSeq )))) by A15, XXREAL_0: 2;

 end;

 hence for l be Nat st l <= k holds ( ||.( Conj (k,z,w)).|| . l) <= ((( ||.z.|| rExpSeq ) . l) * (2 * ( Sum ( ||.w.|| rExpSeq ))));

 end;

 now



 A16: 0 <> ( Sum ( ||.w.|| rExpSeq )) by Th28;



 A17: ((2 * ( Sum ( ||.w.|| rExpSeq ))) * (p / (4 * ( Sum ( ||.w.|| rExpSeq ))))) = ((2 * ( Sum ( ||.w.|| rExpSeq ))) * (p * ((4 * ( Sum ( ||.w.|| rExpSeq ))) " ))) by XCMPLX_0:def 9

 .= (((2 * ( Sum ( ||.w.|| rExpSeq ))) * p) * ((4 * ( Sum ( ||.w.|| rExpSeq ))) " ))

 .= (((2 * p) * ( Sum ( ||.w.|| rExpSeq ))) / (4 * ( Sum ( ||.w.|| rExpSeq )))) by XCMPLX_0:def 9

 .= ((2 * p) / 4) by A16, XCMPLX_1: 91

 .= (p / 2);



 A18: 0 <> ( Sum ( ||.z.|| rExpSeq )) by Th28;



 A19: (( Sum ( ||.z.|| rExpSeq )) * (p / (4 * ( Sum ( ||.z.|| rExpSeq ))))) = (( Sum ( ||.z.|| rExpSeq )) * (p * ((4 * ( Sum ( ||.z.|| rExpSeq ))) " ))) by XCMPLX_0:def 9

 .= ((( Sum ( ||.z.|| rExpSeq )) * p) * ((4 * ( Sum ( ||.z.|| rExpSeq ))) " ))

 .= ((( Sum ( ||.z.|| rExpSeq )) * p) / (4 * ( Sum ( ||.z.|| rExpSeq )))) by XCMPLX_0:def 9

 .= (p / 4) by A18, XCMPLX_1: 91;

 let k such that

 A20: n4 <= k;



 A21: ( 0 + n3) <= (n3 + n3) by XREAL_1: 6;

 then (k -' n3) = (k - n3) by A20, XREAL_1: 233, XXREAL_0: 2;

 then

 A22: k = ((k -' n3) + n3);



 A23: n3 <= k by A20, A21, XXREAL_0: 2;

 now

 let l be Nat;

 assume

 A24: l <= n3;

 then

 A25: ((n3 + n3) - n3) <= ((n3 + n3) - l) by XREAL_1: 10;

 (n4 - l) <= (k - l) by A20, XREAL_1: 9;

 then

 A26: n3 <= (k - l) by A25, XXREAL_0: 2;



 A27: ( 0 + n2) <= (n1 + n2) by XREAL_1: 6;

 l <= k by A23, A24, XXREAL_0: 2;

 then

 A28: ( ||.( Conj (k,z,w)).|| . l) <= ((( ||.z.|| rExpSeq ) . l) * ||.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).||) by A7;



 A29: 0 <= (( ||.z.|| rExpSeq ) . l) by Th26;

 ( 0 + n3) <= (n3 + n3) by XREAL_1: 6;

 then n2 <= n4 by A27, XXREAL_0: 2;

 then

 A30: n2 <= k by A20, XXREAL_0: 2;

 (k -' l) = (k - l) by A23, A24, XREAL_1: 233, XXREAL_0: 2;

 then n2 <= (k -' l) by A27, A26, XXREAL_0: 2;

 then ||.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).|| < p1 by A5, A30;

 then ((( ||.z.|| rExpSeq ) . l) * ||.((( Partial_Sums (w ExpSeq )) . k) - (( Partial_Sums (w ExpSeq )) . (k -' l))).||) <= ((( ||.z.|| rExpSeq ) . l) * p1) by A29, XREAL_1: 64;

 hence ( ||.( Conj (k,z,w)).|| . l) <= (p1 * (( ||.z.|| rExpSeq ) . l)) by A28, XXREAL_0: 2;

 end;

 then

 A31: (( Partial_Sums ||.( Conj (k,z,w)).||) . n3) <= ((( Partial_Sums ( ||.z.|| rExpSeq )) . n3) * p1) by COMSEQ_3: 7;



 A32: (n1 + 0 ) <= (n1 + n2) by XREAL_1: 6;

 then n1 <= k by A23, XXREAL_0: 2;

 then |.((( Partial_Sums ( ||.z.|| rExpSeq )) . k) - (( Partial_Sums ( ||.z.|| rExpSeq )) . n3)).| <= p1 by A6, A32;

 then ((( Partial_Sums ( ||.z.|| rExpSeq )) . k) - (( Partial_Sums ( ||.z.|| rExpSeq )) . n3)) <= p1 by A20, A21, Th29, XXREAL_0: 2;

 then

 A33: (((( Partial_Sums ( ||.z.|| rExpSeq )) . k) - (( Partial_Sums ( ||.z.|| rExpSeq )) . n3)) * (2 * ( Sum ( ||.w.|| rExpSeq )))) <= (p1 * (2 * ( Sum ( ||.w.|| rExpSeq )))) by A2, XREAL_1: 64;

 for l be Nat st l <= k holds ( ||.( Conj (k,z,w)).|| . l) <= ((2 * ( Sum ( ||.w.|| rExpSeq ))) * (( ||.z.|| rExpSeq ) . l)) by A11;

 then ((( Partial_Sums ||.( Conj (k,z,w)).||) . k) - (( Partial_Sums ||.( Conj (k,z,w)).||) . n3)) <= (((( Partial_Sums ( ||.z.|| rExpSeq )) . k) - (( Partial_Sums ( ||.z.|| rExpSeq )) . n3)) * (2 * ( Sum ( ||.w.|| rExpSeq )))) by A22, COMSEQ_3: 8;

 then

 A34: ((( Partial_Sums ||.( Conj (k,z,w)).||) . k) - (( Partial_Sums ||.( Conj (k,z,w)).||) . n3)) <= (p1 * (2 * ( Sum ( ||.w.|| rExpSeq )))) by A33, XXREAL_0: 2;



 A35: ( 0 + (p / 4)) < ((p / 4) + (p / 4)) by A1, XREAL_1: 6;

 ((( Partial_Sums ( ||.z.|| rExpSeq )) . n3) * p1) <= (( Sum ( ||.z.|| rExpSeq )) * p1) by A4, Th27, XREAL_1: 64;

 then

 A36: (( Partial_Sums ||.( Conj (k,z,w)).||) . n3) <= (( Sum ( ||.z.|| rExpSeq )) * p1) by A31, XXREAL_0: 2;

 (( Sum ( ||.z.|| rExpSeq )) * p1) <= (( Sum ( ||.z.|| rExpSeq )) * (p / (4 * ( Sum ( ||.z.|| rExpSeq ))))) by A3, XREAL_1: 64, XXREAL_0: 17;

 then (( Partial_Sums ||.( Conj (k,z,w)).||) . n3) <= (p / 4) by A36, A19, XXREAL_0: 2;

 then

 A37: (( Partial_Sums ||.( Conj (k,z,w)).||) . n3) < (p / 2) by A35, XXREAL_0: 2;

 ((2 * ( Sum ( ||.w.|| rExpSeq ))) * p1) <= ((2 * ( Sum ( ||.w.|| rExpSeq ))) * (p / (4 * ( Sum ( ||.w.|| rExpSeq ))))) by A2, XREAL_1: 64, XXREAL_0: 17;

 then ((( Partial_Sums ||.( Conj (k,z,w)).||) . k) - (( Partial_Sums ||.( Conj (k,z,w)).||) . n3)) <= (p / 2) by A34, A17, XXREAL_0: 2;

 then (((( Partial_Sums ||.( Conj (k,z,w)).||) . k) - (( Partial_Sums ||.( Conj (k,z,w)).||) . n3)) + (( Partial_Sums ||.( Conj (k,z,w)).||) . n3)) < ((p / 2) + (p / 2)) by A37, XREAL_1: 8;

 hence |.(( Partial_Sums ||.( Conj (k,z,w)).||) . k).| < p by Th30;

 end;

 hence thesis;

 end;

 theorem :: CLOPBAN4:32



 Th32: for seq st for k holds (seq . k) = (( Partial_Sums ( Conj (k,z,w))) . k) holds seq is convergent & ( lim seq) = ( 0. X)

 proof

 deffunc U( Nat) = (( Partial_Sums ||.( Conj ($1,z,w)).||) . $1);

 ex rseq be Real_Sequence st for k holds (rseq . k) = U(k) from SEQ_1:sch 1;

 then

 consider rseq be Real_Sequence such that

 A1: for k holds (rseq . k) = (( Partial_Sums ||.( Conj (k,z,w)).||) . k);

 let seq such that

 A2: for k holds (seq . k) = (( Partial_Sums ( Conj (k,z,w))) . k);

 A3:

 now

 let k;

 ||.(seq . k).|| = ||.(( Partial_Sums ( Conj (k,z,w))) . k).|| by A2;

 hence ||.(seq . k).|| <= (( Partial_Sums ||.( Conj (k,z,w)).||) . k) by Th10;

 end;

 A4:

 now

 let k;

 ||.(seq . k).|| <= (( Partial_Sums ||.( Conj (k,z,w)).||) . k) by A3;

 hence ||.(seq . k).|| <= (rseq . k) by A1;

 end;

 A5:

 now

 let p be Real;

 assume p > 0 ;

 then

 consider n such that

 A6: for k st n <= k holds |.(( Partial_Sums ||.( Conj (k,z,w)).||) . k).| < p by Th31;

 take n;

 now

 let k such that

 A7: n <= k;

 |.((rseq . k) - 0 ).| = |.(( Partial_Sums ||.( Conj (k,z,w)).||) . k).| by A1;

 hence |.((rseq . k) - 0 ).| < p by A6, A7;

 end;

 hence for k st n <= k holds |.((rseq . k) - 0 ).| < p;

 end;

 then

 A8: rseq is convergent by SEQ_2:def 6;

 then ( lim rseq) = 0 by A5, SEQ_2:def 7;

 hence thesis by A4, A8, Th12;

 end;



 Lm3: for z, w st (z,w) are_commutative holds (( Sum (z ExpSeq )) * ( Sum (w ExpSeq ))) = ( Sum ((z + w) ExpSeq ))

 proof

 let z, w such that

 A1: (z,w) are_commutative ;

 deffunc U( Nat) = (( Partial_Sums ( Conj ($1,z,w))) . $1);

 ex seq st for k be Element of NAT holds (seq . k) = U(k) from FUNCT_2:sch 4;

 then

 consider seq be sequence of X such that

 A2: for k be Element of NAT holds (seq . k) = (( Partial_Sums ( Conj (k,z,w))) . k);



 A3: for k be Nat holds (seq . k) = (( Partial_Sums ( Conj (k,z,w))) . k)

 proof

 let k be Nat;

 k in NAT by ORDINAL1:def 12;

 hence thesis by A2;

 end;

 now

 let k be Element of NAT ;



 thus (seq . k) = (( Partial_Sums ( Conj (k,z,w))) . k) by A2

 .= (((( Partial_Sums (z ExpSeq )) . k) * (( Partial_Sums (w ExpSeq )) . k)) - (( Partial_Sums ((z + w) ExpSeq )) . k)) by A1, Th25

 .= (((( Partial_Sums (z ExpSeq )) * ( Partial_Sums (w ExpSeq ))) . k) - (( Partial_Sums ((z + w) ExpSeq )) . k)) by LOPBAN_3:def 7

 .= (((( Partial_Sums (z ExpSeq )) * ( Partial_Sums (w ExpSeq ))) - ( Partial_Sums ((z + w) ExpSeq ))) . k) by NORMSP_1:def 3;

 end;

 then

 A4: seq = ((( Partial_Sums (z ExpSeq )) * ( Partial_Sums (w ExpSeq ))) - ( Partial_Sums ((z + w) ExpSeq ))) by FUNCT_2: 63;



 A5: ( Partial_Sums (w ExpSeq )) is convergent by CLOPBAN3:def 1;



 A6: ( lim seq) = ( 0. X) by A3, Th32;



 A7: ( Partial_Sums ((z + w) ExpSeq )) is convergent by CLOPBAN3:def 1;



 A8: ( Partial_Sums (z ExpSeq )) is convergent by CLOPBAN3:def 1;

 then

 A9: (( Partial_Sums (z ExpSeq )) * ( Partial_Sums (w ExpSeq ))) is convergent by A5, Th3;



 A10: ( lim (( Partial_Sums (z ExpSeq )) * ( Partial_Sums (w ExpSeq )))) = (( lim ( Partial_Sums (z ExpSeq ))) * ( lim ( Partial_Sums (w ExpSeq )))) by A8, A5, Th8;



 thus ( Sum ((z + w) ExpSeq )) = ( lim ( Partial_Sums ((z + w) ExpSeq ))) by CLOPBAN3:def 2

 .= (( lim ( Partial_Sums (z ExpSeq ))) * ( lim ( Partial_Sums (w ExpSeq )))) by A4, A7, A9, A10, A6, Th1

 .= (( Sum (z ExpSeq )) * ( lim ( Partial_Sums (w ExpSeq )))) by CLOPBAN3:def 2

 .= (( Sum (z ExpSeq )) * ( Sum (w ExpSeq ))) by CLOPBAN3:def 2;

 end;

 definition

 let X;

 :: CLOPBAN4:def6

 func exp_ X -> Function of the carrier of X, the carrier of X means

 : Def6: for z be Element of X holds (it . z) = ( Sum (z ExpSeq ));

 existence

 proof

 deffunc U( Element of X) = ( Sum ($1 ExpSeq ));

 ex f be Function of the carrier of X, the carrier of X st for z be Element of X holds (f . z) = U(z) from FUNCT_2:sch 4;

 hence thesis;

 end;

 uniqueness

 proof

 let f1,f2 be Function of the carrier of X, the carrier of X;

 assume that

 A1: for z be Element of X holds (f1 . z) = ( Sum (z ExpSeq )) and

 A2: for z be Element of X holds (f2 . z) = ( Sum (z ExpSeq ));

 for z be Element of X holds (f1 . z) = (f2 . z)

 proof

 let z be Element of X;



 thus (f1 . z) = ( Sum (z ExpSeq )) by A1

 .= (f2 . z) by A2;

 end;

 hence f1 = f2 by FUNCT_2: 63;

 end;

 end

 definition

 let X, z;

 :: CLOPBAN4:def7

 func exp z -> Element of X equals (( exp_ X) . z);

 correctness ;

 end

 theorem :: CLOPBAN4:33

 for z holds ( exp z) = ( Sum (z ExpSeq )) by Def6;

 theorem :: CLOPBAN4:34



 Th34: for z1, z2 st (z1,z2) are_commutative holds ( exp (z1 + z2)) = (( exp z1) * ( exp z2)) & ( exp (z2 + z1)) = (( exp z2) * ( exp z1)) & ( exp (z1 + z2)) = ( exp (z2 + z1)) & (( exp z1),( exp z2)) are_commutative

 proof

 let z1, z2 such that

 A1: (z1,z2) are_commutative ;



 A2: ( exp (z2 + z1)) = ( Sum ((z2 + z1) ExpSeq )) by Def6

 .= (( Sum (z2 ExpSeq )) * ( Sum (z1 ExpSeq ))) by A1, Lm3

 .= (( exp z2) * ( Sum (z1 ExpSeq ))) by Def6

 .= (( exp z2) * ( exp z1)) by Def6;

 ( exp (z1 + z2)) = ( Sum ((z1 + z2) ExpSeq )) by Def6

 .= (( Sum (z1 ExpSeq )) * ( Sum (z2 ExpSeq ))) by A1, Lm3

 .= (( exp z1) * ( Sum (z2 ExpSeq ))) by Def6

 .= (( exp z1) * ( exp z2)) by Def6;

 hence thesis by A2, LOPBAN_4:def 1;

 end;

 theorem :: CLOPBAN4:35

 for z1, z2 st (z1,z2) are_commutative holds (z1 * ( exp z2)) = (( exp z2) * z1)

 proof

 let z1, z2 such that

 A1: (z1,z2) are_commutative ;

 now

 let n be Element of NAT ;



 thus ((z1 * (z2 ExpSeq )) . n) = (z1 * ((z2 ExpSeq ) . n)) by LOPBAN_3:def 5

 .= (z1 * (( 1r / (n ! )) * (z2 #N n))) by Def1

 .= (( 1r / (n ! )) * (z1 * (z2 #N n))) by CLOPBAN3: 38

 .= (( 1r / (n ! )) * ((z2 #N n) * z1)) by A1, Lm2

 .= ((( 1r / (n ! )) * (z2 #N n)) * z1) by CLOPBAN3: 38

 .= (((z2 ExpSeq ) . n) * z1) by Def1

 .= (((z2 ExpSeq ) * z1) . n) by LOPBAN_3:def 6;

 end;

 then

 A2: (z1 * (z2 ExpSeq )) = ((z2 ExpSeq ) * z1) by FUNCT_2: 63;



 A3: ( Partial_Sums (z2 ExpSeq )) is convergent by CLOPBAN3:def 1;



 thus (z1 * ( exp z2)) = (z1 * ( Sum (z2 ExpSeq ))) by Def6

 .= (z1 * ( lim ( Partial_Sums (z2 ExpSeq )))) by CLOPBAN3:def 2

 .= ( lim (z1 * ( Partial_Sums (z2 ExpSeq )))) by A3, Th6

 .= ( lim ( Partial_Sums (z1 * (z2 ExpSeq )))) by Th9

 .= ( lim (( Partial_Sums (z2 ExpSeq )) * z1)) by A2, Th9

 .= (( lim ( Partial_Sums (z2 ExpSeq ))) * z1) by A3, Th7

 .= (( Sum (z2 ExpSeq )) * z1) by CLOPBAN3:def 2

 .= (( exp z2) * z1) by Def6;

 end;

 theorem :: CLOPBAN4:36



 Th36: ( exp ( 0. X)) = ( 1. X)

 proof

 ( exp ( 0. X)) = ( Sum (( 0. X) ExpSeq )) by Def6

 .= ( 1. X) by Th19;

 hence thesis;

 end;

 theorem :: CLOPBAN4:37



 Th37: (( exp z) * ( exp ( - z))) = ( 1. X) & (( exp ( - z)) * ( exp z)) = ( 1. X)

 proof

 (z * ( - z)) = (z * (( - 1r ) * z)) by CLVECT_1: 3

 .= (( - 1r ) * (z * z)) by CLOPBAN3: 38

 .= ((( - 1r ) * z) * z) by CLOPBAN3: 38

 .= (( - z) * z) by CLVECT_1: 3;

 then

 A1: (z,( - z)) are_commutative by LOPBAN_4:def 1;



 hence (( exp z) * ( exp ( - z))) = ( exp (z + ( - z))) by Th34

 .= ( exp ( 0. X)) by RLVECT_1: 5

 .= ( 1. X) by Th36;



 thus (( exp ( - z)) * ( exp z)) = ( exp (( - z) + z)) by A1, Th34

 .= ( exp ( 0. X)) by RLVECT_1: 5

 .= ( 1. X) by Th36;

 end;

 theorem :: CLOPBAN4:38

 ( exp z) is invertible & (( exp z) " ) = ( exp ( - z)) & ( exp ( - z)) is invertible & (( exp ( - z)) " ) = ( exp z)

 proof



 A1: (( exp ( - z)) * ( exp z)) = ( 1. X) by Th37;



 A2: (( exp z) * ( exp ( - z))) = ( 1. X) by Th37;

 hence ( exp z) is invertible by A1, LOPBAN_3:def 4;

 hence (( exp z) " ) = ( exp ( - z)) by A2, A1, LOPBAN_3:def 8;

 thus ( exp ( - z)) is invertible by A2, A1, LOPBAN_3:def 4;

 hence thesis by A2, A1, LOPBAN_3:def 8;

 end;

 theorem :: CLOPBAN4:39



 Th39: for z holds for s,t be Complex holds ((s * z),(t * z)) are_commutative

 proof

 let z;

 let s,t be Complex;

 ((s * z) * (t * z)) = ((s * t) * (z * z)) by CLOPBAN3: 38

 .= ((t * z) * (s * z)) by CLOPBAN3: 38;

 hence thesis by LOPBAN_4:def 1;

 end;

 theorem :: CLOPBAN4:40

 for z holds for s,t be Complex holds (( exp (s * z)) * ( exp (t * z))) = ( exp ((s + t) * z)) & (( exp (t * z)) * ( exp (s * z))) = ( exp ((t + s) * z)) & ( exp ((s + t) * z)) = ( exp ((t + s) * z)) & (( exp (s * z)),( exp (t * z))) are_commutative

 proof

 let z;

 let s,t be Complex;



 A1: ((s * z),(t * z)) are_commutative by Th39;



 hence

 A2: (( exp (s * z)) * ( exp (t * z))) = ( exp ((s * z) + (t * z))) by Th34

 .= ( exp ((s + t) * z)) by CLOPBAN3: 38;



 thus

 A3: (( exp (t * z)) * ( exp (s * z))) = ( exp ((t * z) + (s * z))) by A1, Th34

 .= ( exp ((t + s) * z)) by CLOPBAN3: 38;

 thus ( exp ((s + t) * z)) = ( exp ((t + s) * z));

 thus thesis by A2, A3, LOPBAN_4:def 1;

 end;