environ
vocabularies HIDDEN, NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI, RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1, FUNCOP_1, PARTFUN1, FINSEQ_1, VALUED_0, CARD_3, MEMBERED, RFINSEQ2, AFINSQ_1, NEWTON, PRE_POLY, FOMODEL0, ORDINAL4, ORDINAL2, VALUED_2, GOBRD13, UPROOTS, FUNCT_6, FUNCT_2, FINSEQ_2, XREAL_0, SETWISEO, CLASSES1, FUNCT_4, BINOP_1, BINOP_2, FINSOP_1, POWER, NUMERAL1, ALGSTR_0, MONOID_0, FLEXARY1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XREAL_0, MEMBERED, RELAT_1, FUNCT_1, RELSET_1, MONOID_0, PARTFUN1, FUNCT_2, BINOP_1, XXREAL_0, NAT_1, CARD_3, FUNCOP_1, SETWISEO, FINSEQ_2, FINSEQ_1, FINSEQOP, VALUED_0, VALUED_2, SETWOP_2, FINSET_1, RVSUM_1, CLASSES1, XXREAL_2, PRE_POLY, RFINSEQ2, FUNCT_6, NAT_D, MATRIX_0, FUNCT_7, FOMODEL2, WSIERP_1, BINOP_2, NEWTON, POWER, FINSOP_1, AFINSQ_1, AFINSQ_2, NUMERAL1, STRUCT_0, ALGSTR_0;
definitions TARSKI, XBOOLE_0, FUNCT_1, VALUED_0;
theorems AFINSQ_1, AFINSQ_2, ALGSTR_0, CARD_1, CARD_3, CLASSES1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_5, FINSEQOP, FINSOP_1, FOMODEL2, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_6, FUNCT_7, GRAPHSP, INTEGRA2, MATRIX_0, MONOID_0, NAT_1, NAT_D, NEWTON, NUMERAL1, ORDINAL1, PARTFUN1, PEPIN, PRE_POLY, PREPOWER, RELAT_1, RFINSEQ, RFINSEQ2, RVSUM_1, RVSUM_2, TARSKI, VALUED_0, VALUED_2, XBOOLE_0, XBOOLE_1, XCMPLX_0, XREAL_0, XREAL_1, XXREAL_0, XXREAL_2, ZFMISC_1;
schemes CLASSES1, FINSEQ_1, FUNCT_2, NAT_1;
registrations ORDINAL1, XREAL_0, FUNCT_1, FINSEQ_1, FINSEQ_2, VALUED_0, FUNCT_7, PRE_POLY, NAT_1, INT_6, RVSUM_1, XCMPLX_0, MEMBERED, VALUED_2, FOMODEL0, XBOOLE_0, RELAT_1, FUNCT_2, FUNCOP_1, CARD_1, XXREAL_2, EUCLID_9, FINSET_1, XXREAL_0, NUMBERS, BINOP_2, INT_1, NEWTON, POWER, AFINSQ_1, AFINSQ_2;
constructors HIDDEN, XXREAL_2, PRE_POLY, ABIAN, RFINSEQ2, CLASSES1, MONOID_0, NAT_D, VALUED_2, FOMODEL2, RELSET_1, WSIERP_1, SETWISEO, BINOP_2, FINSEQOP, FINSOP_1, NEWTON, POWER, RECDEF_1, AFINSQ_2, NUMERAL1, JORDAN1H;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities FINSEQ_1, FINSEQ_2, XCMPLX_0;
expansions FINSEQ_1, TARSKI, XBOOLE_0, FUNCT_1;
Lm1:
for D being non empty set
for f being FinSequence of D * st f = {} holds
(D -concatenation) "**" f = {}
Lm2:
for k, n being Nat
for g, h being complex-valued FinSequence st k <= n & n <= len g holds
((g ^ h),k) +...+ ((g ^ h),n) = (g,k) +...+ (g,n)
Lm3:
for k, n being Nat
for g, h being complex-valued FinSequence st k <= n & k > len g holds
((g ^ h),k) +...+ ((g ^ h),n) = (h,(k -' (len g))) +...+ (h,(n -' (len g)))
Lm4:
for n being Nat
for f, g being natural-valued FinSequence st f is increasing & f | n = g holds
g is increasing
Lm5:
for i, n being Nat
for f1, f2 being natural-valued FinSequence st len f1 = i + 1 & f1 | i = f2 holds
Sum (n |^ f1) = (Sum (n |^ f2)) + (n |^ (f1 . (i + 1)))
Lm6:
for n being Nat
for f1, f2 being natural-valued increasing FinSequence st n > 1 & Sum (n |^ f1) > 0 & Sum (n |^ f1) = Sum (n |^ f2) holds
f1 . (len f1) <= f2 . (len f2)
Lm7:
for i being Nat
for f being FinSequence
for o1, o2 being valued_reorganization of f st rng ((f *. o1) . i) = rng ((f *. o2) . i) holds
rng (o1 . i) c= rng (o2 . i)