environ
vocabularies HIDDEN, NUMBERS, CLOPBAN2, SUBSET_1, NAT_1, SEQ_1, RELAT_1, COMSEQ_3, ARYTM_3, CARD_1, PREPOWER, FUNCT_1, MESFUNC1, LOPBAN_4, SEQ_2, ORDINAL2, ARYTM_1, SUPINF_2, REAL_1, XXREAL_0, NORMSP_1, PRE_TOPC, XXREAL_2, SERIES_1, COMPLEX1, SIN_COS, XBOOLE_0, STRUCT_0, NEWTON, REALSET1, VALUED_1, XCMPLX_0, LOPBAN_3, CARD_3, VALUED_0, RSSPACE3, ALGSTR_0;
notations HIDDEN, RELAT_1, FUNCT_1, SUBSET_1, FUNCT_2, PRE_TOPC, XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1, NUMBERS, CLOPBAN3, COMPLEX1, REAL_1, NAT_1, STRUCT_0, ALGSTR_0, NEWTON, RLVECT_1, SEQ_1, SEQ_2, SEQM_3, SERIES_1, LOPBAN_4, NAT_D, SIN_COS, BHSP_4, NORMSP_0, CLVECT_1, CSSPACE3, CLOPBAN2, LOPBAN_3, NORMSP_1;
definitions CLVECT_1;
theorems ABSVALUE, RLVECT_1, XCMPLX_0, XCMPLX_1, XREAL_0, SEQ_2, SEQM_3, COMSEQ_3, SIN_COS, SERIES_1, NAT_1, INT_1, NEWTON, FUNCT_2, SEQ_4, LOPBAN_3, CLOPBAN3, CLVECT_1, COMPLEX1, CSSPACE3, XREAL_1, XXREAL_0, LOPBAN_4, BHSP_4, NORMSP_1, VALUED_0, ORDINAL1, NORMSP_0, GROUP_1, VECTSP_1;
schemes SEQ_1, NAT_1, FUNCT_2, CLASSES1;
registrations ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, CLOPBAN2, CLOPBAN3, VALUED_0, SEQ_2, NEWTON, NAT_1, FUNCT_2;
constructors HIDDEN, REAL_1, SQUARE_1, SEQ_2, COMSEQ_3, NAT_D, SIN_COS, BHSP_4, LOPBAN_4, CSSPACE3, CLOPBAN3, RELSET_1, COMSEQ_2, NUMBERS, LOPBAN_3;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities ;
expansions CLVECT_1;
Lm1:
for X being Complex_Banach_Algebra
for z being Element of X
for n being Nat holds
( z * (z #N n) = z #N (n + 1) & (z #N n) * z = z #N (n + 1) & z * (z #N n) = (z #N n) * z )
Lm2:
for X being Complex_Banach_Algebra
for n being Nat
for z, w being Element of X st z,w are_commutative holds
( w * (z #N n) = (z #N n) * w & z * (w #N n) = (w #N n) * z )
Lm3:
for X being Complex_Banach_Algebra
for z, w being Element of X st z,w are_commutative holds
(Sum (z ExpSeq)) * (Sum (w ExpSeq)) = Sum ((z + w) ExpSeq)