environ
vocabularies HIDDEN, NUMBERS, NAT_1, FINSEQ_1, VALUED_0, FINSEQ_2, CARD_1, RELAT_1, SUBSET_1, XBOOLE_0, FUNCT_1, TARSKI, XREAL_0, ORDINAL4, ARYTM_1, ARYTM_3, SQUARE_1, FUNCOP_1, REAL_1, XXREAL_0, CARD_3, COMPLEX1, PREPOWER, ORDINAL1, RVSUM_3, POWER, UNIALG_1, FINSET_1, NEWTON, AFINSQ_1, FUNCT_4, CLASSES1, PARTFUN3, RFINSEQ, XXREAL_2, MEMBERED;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_2, VALUED_0, XBOOLE_0, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, SQUARE_1, NAT_D, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, SETWISEO, FUNCT_2, MEMBERED, BINOP_1, FINSET_1, CLASSES1, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, VALUED_1, FINSOP_1, PBOOLE, PREPOWER, FUNCT_4, SERIES_1, FINSEQ_7, SEQ_4, NEWTON, POWER, RVSUM_1, FUNCT_7, RFINSEQ, COMPLEX1, PARTFUN3;
definitions BINOP_1, FINSEQOP, FINSEQ_1, TARSKI, RFINSEQ, CLASSES1, XBOOLE_0, SEQM_3, PARTFUN3;
theorems SQUARE_1, FUNCT_1, FINSEQ_1, FUNCOP_1, FINSEQ_2, RELAT_1, XREAL_0, ZFMISC_1, XREAL_1, XBOOLE_1, FINSEQ_3, CARD_1, TARSKI, RVSUM_1, XCMPLX_1, FINSEQ_5, POWER, NAT_1, NEWTON, FUNCT_7, RFINSEQ, CLASSES1, XXREAL_0, COMPLEX1, NAT_4, CARD_2, XBOOLE_0, PREPOWER;
schemes NAT_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, NAT_1, BINOP_2, FINSEQ_1, FINSEQ_2, VALUED_0, VALUED_1, RELAT_1, FINSEQ_4, CARD_1, INT_1, RVSUM_1, FUNCT_7, SEQ_4, FINSET_1, XXREAL_2, RELSET_1, XXREAL_0, MEMBERED, COMPLEX1, NEWTON, FINSEQ_6, FINSEQ_7, PDIFF_7;
constructors HIDDEN, PARTFUN1, BINOP_1, SETWISEO, SQUARE_1, NAT_1, BINOP_2, MEMBERED, XXREAL_2, VALUED_1, FINSEQOP, FINSEQ_4, FINSOP_1, SETWOP_2, RELSET_1, XXREAL_1, REAL_1, FINSEQ_2, RVSUM_1, POWER, FINSET_1, NEWTON, ABIAN, RFINSEQ, PBOOLE, NAT_D, XREAL_0, CARD_1, CARD_2, SEQ_4, FUNCT_4, FUNCT_7, CLASSES1, SERIES_1, SERIES_3, SEQ_1, PREPOWER, FINSEQ_7, PARTFUN3;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities FINSEQ_1, SQUARE_1, FINSEQ_2, VALUED_1, FINSEQ_4, XREAL_0, ORDINAL1, FUNCT_7, FINSEQ_7, RVSUM_1, FUNCOP_1, RELAT_1;
expansions BINOP_1, FINSEQOP, FINSEQ_1, TARSKI, RFINSEQ, CLASSES1, FUNCT_7, FINSEQ_7, XBOOLE_0, SEQM_3, PARTFUN3;
MeanL:
for f being heterogeneous real-valued FinSequence holds MeanLess f <> {}
MeanM:
for f being heterogeneous real-valued FinSequence holds MeanMore f <> {}
registration
let f be
real-valued FinSequence;
let i,
j be
Nat;
let a,
b be
Real;
coherence
( Replace (f,i,j,a,b) is real-valued & Replace (f,i,j,a,b) is FinSequence-like )
;
end;
theorem ReplacePositive2:
definition
let f be
heterogeneous non
empty real-valued positive FinSequence;
existence
ex b1 being real-valued FinSequence ex i, j being Nat st
( i = the Element of MeanLess f & j = the Element of MeanMore f & b1 = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) )
uniqueness
for b1, b2 being real-valued FinSequence st ex i, j being Nat st
( i = the Element of MeanLess f & j = the Element of MeanMore f & b1 = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) ) & ex i, j being Nat st
( i = the Element of MeanLess f & j = the Element of MeanMore f & b2 = Replace (f,i,j,(Mean f),(((f . i) + (f . j)) - (Mean f))) ) holds
b1 = b2
;
end;