environ
vocabularies HIDDEN, NUMBERS, SUPINF_1, REAL_1, RELAT_1, XXREAL_0, ARYTM_3, COMPLEX1, CARD_1, ARYTM_1, FINSEQ_1, CARD_3, FUNCT_1, SUBSET_1, SUPINF_2, NAT_1, FUNCT_2, FUNCOP_1, XBOOLE_0, TARSKI, ORDINAL4, PARTFUN1, RFINSEQ, XCMPLX_0, MESFUNC1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0, XXREAL_3, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, BINOP_1, FUNCT_2, DOMAIN_1, RFINSEQ, RFUNCT_3, RVSUM_1, FUNCOP_1, FINSEQ_1, FINSEQ_4, NAT_1, NAT_D, SUPINF_1, SUPINF_2, MEASURE6;
definitions ;
theorems FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_5, NAT_1, TARSKI, FUNCT_1, INT_1, XCMPLX_1, XBOOLE_0, RFINSEQ, RELAT_1, FUNCOP_1, XREAL_1, XXREAL_0, XREAL_0, PARTFUN1, ORDINAL1, XXREAL_3, SUPINF_2, ABSVALUE, COMPLEX1;
schemes FUNCT_2, FINSEQ_2, NAT_1, RECDEF_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, VALUED_0, CARD_1, XXREAL_3;
constructors HIDDEN, BINOP_1, DOMAIN_1, REAL_1, NAT_1, FINSEQ_4, FINSOP_1, RVSUM_1, SUPINF_2, RFINSEQ, RFUNCT_3, MEASURE6, BINARITH, BINOP_2, SUPINF_1, CLASSES1, NAT_D, RELSET_1, XXREAL_3, FINSEQ_1, FUNCT_1, FUNCT_2, INT_1, FUNCOP_1, COMPLEX1, ARYTM_2;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities SUPINF_2, XXREAL_3;
expansions ;
theorem
for
x,
y being
ExtReal for
a,
b being
Real st
x = a &
y = b holds
x / y = a / b ;
Lm1:
for F being FinSequence of ExtREAL
for x being Element of ExtREAL holds Sum (F ^ <*x*>) = (Sum F) + x
Lm2:
for F being FinSequence of ExtREAL st not -infty in rng F holds
Sum F <> -infty
Lm3:
for n, q being Nat st q in Seg (n + 1) holds
ex p being Permutation of (Seg (n + 1)) st
for i being Element of NAT st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )
Lm4:
for n, q being Nat
for s, p being Permutation of (Seg (n + 1))
for s9 being FinSequence of Seg (n + 1) st s9 = s & q = s . (n + 1) & ( for i being Element of NAT st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ) holds
p * (s9 | n) is Permutation of (Seg n)
Lm5:
for n, q being Nat
for p being Permutation of (Seg (n + 1))
for F, H being FinSequence of ExtREAL st F = H * p & q in Seg (n + 1) & len H = n + 1 & not -infty in rng H & ( for i being Element of NAT st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ) holds
Sum F = Sum H