environ
vocabularies HIDDEN, NUMBERS, LOPBAN_2, SUBSET_1, NAT_1, SEQ_1, XBOOLE_0, ALGSTR_0, RELAT_1, COMSEQ_3, ARYTM_3, CARD_1, PREPOWER, FUNCT_1, MESFUNC1, SEQ_2, ORDINAL2, ARYTM_1, SUPINF_2, REAL_1, XXREAL_0, NORMSP_1, PRE_TOPC, XXREAL_2, SERIES_1, COMPLEX1, SIN_COS, REALSET1, STRUCT_0, VALUED_1, NEWTON, LOPBAN_3, CARD_3, VALUED_0, RSSPACE3, LOPBAN_4;
notations HIDDEN, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, XXREAL_0, XREAL_0, VALUED_0, PRE_TOPC, ALGSTR_0, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, NORMSP_0, NORMSP_1, RSSPACE3, SEQ_1, SEQ_2, NEWTON, REAL_1, NAT_1, STRUCT_0, SERIES_1, NAT_D, SIN_COS, RLVECT_1, BHSP_4, LOPBAN_2, LOPBAN_3;
definitions NORMSP_1, VALUED_0;
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, NORMSP_1, SEQ_4, RSSPACE3, LOPBAN_3, XREAL_1, XXREAL_0, ORDINAL1, BHSP_4, NORMSP_0;
schemes SEQ_1, NAT_1, SIN_COS, FUNCT_2, CLASSES1;
registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, MEMBERED, SIN_COS, STRUCT_0, GROUP_1, LOPBAN_2, LOPBAN_3, VALUED_0, SEQ_2, NUMBERS, FUNCT_2, NEWTON;
constructors HIDDEN, REAL_1, SQUARE_1, SEQ_2, COMSEQ_3, NAT_D, SIN_COS, BHSP_4, RSSPACE3, LOPBAN_3, RELSET_1, COMSEQ_2;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities LOPBAN_3;
expansions NORMSP_1, LOPBAN_3, VALUED_0;
Lm1:
for X being 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 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 )
theorem Th13:
( ( for
k being
Nat st
0 < k holds
((k -' 1) !) * k = k ! ) & ( for
m,
k being
Nat st
k <= m holds
((m -' k) !) * ((m + 1) - k) = ((m + 1) -' k) ! ) )
Lm3:
for X being Banach_Algebra
for z, w being Element of X st z,w are_commutative holds
(Sum (z rExpSeq)) * (Sum (w rExpSeq)) = Sum ((z + w) rExpSeq)