:: RFINSEQ2 semantic presentation begin definition let f be FinSequence of REAL ; func max_p f -> Element of NAT means :Def1: :: RFINSEQ2:def 1 ( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . it holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . it holds it <= j ) ) ) ); existence ex b1 being Element of NAT st ( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds b1 <= j ) ) ) ) proof A1: dom f = Seg (len f) by FINSEQ_1:def_3; percases ( len f = 0 or len f <> 0 ) ; suppose len f = 0 ; ::_thesis: ex b1 being Element of NAT st ( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds b1 <= j ) ) ) ) hence ex b1 being Element of NAT st ( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds b1 <= j ) ) ) ) ; ::_thesis: verum end; supposeA2: len f <> 0 ; ::_thesis: ex b1 being Element of NAT st ( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds b1 <= j ) ) ) ) defpred S1[ Element of NAT ] means ex n being Element of NAT st ( ( $1 <> 0 implies ( n <= $1 & n in dom f ) ) & ( for i being Element of NAT for r1, r2 being Real st i <= $1 & i in dom f & r1 = f . i & r2 = f . n holds r1 <= r2 ) & ( for j being Element of NAT st j <= $1 & j in dom f & f . j = f . n holds n <= j ) ); A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then consider n1 being Element of NAT such that A4: ( k <> 0 implies ( n1 <= k & n1 in dom f ) ) and A5: for i being Element of NAT for r1, r2 being Real st i <= k & i in dom f & r1 = f . i & r2 = f . n1 holds r1 <= r2 and A6: for j being Element of NAT st j <= k & j in dom f & f . j = f . n1 holds n1 <= j ; percases ( k = 0 or k <> 0 ) ; supposeA7: k = 0 ; ::_thesis: S1[k + 1] A8: dom f = Seg (len f) by FINSEQ_1:def_3; A9: for i being Element of NAT for r1, r2 being Real st i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 holds r1 <= r2 proof let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 holds r1 <= r2 let r1, r2 be Real; ::_thesis: ( i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 implies r1 <= r2 ) assume that A10: i <= 1 and A11: i in dom f and A12: ( r1 = f . i & r2 = f . 1 ) ; ::_thesis: r1 <= r2 1 <= i by A11, FINSEQ_3:25; hence r1 <= r2 by A10, A12, XXREAL_0:1; ::_thesis: verum end; len f >= 0 + 1 by A2, NAT_1:13; then A13: 1 in dom f by A8, FINSEQ_1:1; for j being Element of NAT st j <= 1 & j in dom f & f . j = f . 1 holds 1 <= j by A8, FINSEQ_1:1; hence S1[k + 1] by A7, A13, A9; ::_thesis: verum end; supposeA14: k <> 0 ; ::_thesis: S1[k + 1] now__::_thesis:_(_(_f_._n1_>=_f_._(k_+_1)_&_S1[k_+_1]_)_or_(_f_._n1_<_f_._(k_+_1)_&_S1[k_+_1]_)_) percases ( f . n1 >= f . (k + 1) or f . n1 < f . (k + 1) ) ; caseA15: f . n1 >= f . (k + 1) ; ::_thesis: S1[k + 1] A16: for i being Element of NAT for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds r1 <= r2 proof let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds r1 <= r2 let r1, r2 be Real; ::_thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 implies r1 <= r2 ) assume that A17: i <= k + 1 and A18: i in dom f and A19: ( r1 = f . i & r2 = f . n1 ) ; ::_thesis: r1 <= r2 percases ( i < k + 1 or i >= k + 1 ) ; suppose i < k + 1 ; ::_thesis: r1 <= r2 then i <= k by NAT_1:13; hence r1 <= r2 by A5, A18, A19; ::_thesis: verum end; suppose i >= k + 1 ; ::_thesis: r1 <= r2 hence r1 <= r2 by A15, A17, A19, XXREAL_0:1; ::_thesis: verum end; end; end; A20: n1 <= k + 1 by A4, A14, NAT_1:13; A21: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . n1 holds n1 <= j proof let j be Element of NAT ; ::_thesis: ( j <= k + 1 & j in dom f & f . j = f . n1 implies n1 <= j ) assume that A22: j <= k + 1 and A23: ( j in dom f & f . j = f . n1 ) ; ::_thesis: n1 <= j now__::_thesis:_(_(_j_<_k_+_1_&_n1_<=_j_)_or_(_j_>=_k_+_1_&_n1_<=_j_)_) percases ( j < k + 1 or j >= k + 1 ) ; case j < k + 1 ; ::_thesis: n1 <= j then j <= k by NAT_1:13; hence n1 <= j by A6, A23; ::_thesis: verum end; case j >= k + 1 ; ::_thesis: n1 <= j hence n1 <= j by A20, A22, XXREAL_0:1; ::_thesis: verum end; end; end; hence n1 <= j ; ::_thesis: verum end; ( k + 1 <> 0 implies ( n1 <= k + 1 & n1 in dom f ) ) by A4, A14, NAT_1:13; hence S1[k + 1] by A16, A21; ::_thesis: verum end; caseA24: f . n1 < f . (k + 1) ; ::_thesis: S1[k + 1] now__::_thesis:_(_(_k_+_1_>_len_f_&_S1[k_+_1]_)_or_(_k_+_1_<=_len_f_&_S1[k_+_1]_)_) percases ( k + 1 > len f or k + 1 <= len f ) ; caseA25: k + 1 > len f ; ::_thesis: S1[k + 1] A26: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . n1 holds n1 <= j proof let j be Element of NAT ; ::_thesis: ( j <= k + 1 & j in dom f & f . j = f . n1 implies n1 <= j ) assume that j <= k + 1 and A27: ( j in dom f & f . j = f . n1 ) ; ::_thesis: n1 <= j percases ( j < k + 1 or j >= k + 1 ) ; suppose j < k + 1 ; ::_thesis: n1 <= j then j <= k by NAT_1:13; hence n1 <= j by A6, A27; ::_thesis: verum end; suppose j >= k + 1 ; ::_thesis: n1 <= j then k < j by NAT_1:13; hence n1 <= j by A4, A14, XXREAL_0:2; ::_thesis: verum end; end; end; A28: k >= len f by A25, NAT_1:13; A29: for i being Element of NAT for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds r1 <= r2 proof let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds r1 <= r2 let r1, r2 be Real; ::_thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 implies r1 <= r2 ) assume that i <= k + 1 and A30: i in dom f and A31: ( r1 = f . i & r2 = f . n1 ) ; ::_thesis: r1 <= r2 i <= len f by A1, A30, FINSEQ_1:1; then i <= k by A28, XXREAL_0:2; hence r1 <= r2 by A5, A30, A31; ::_thesis: verum end; n1 <= len f by A1, A4, A14, FINSEQ_1:1; then ( k + 1 <> 0 implies ( n1 <= k + 1 & n1 in dom f ) ) by A4, A14, A25, XXREAL_0:2; hence S1[k + 1] by A29, A26; ::_thesis: verum end; caseA32: k + 1 <= len f ; ::_thesis: S1[k + 1] set n2 = k + 1; A33: for i being Element of NAT for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) holds r1 <= r2 proof let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) holds r1 <= r2 let r1, r2 be Real; ::_thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) implies r1 <= r2 ) assume that A34: i <= k + 1 and A35: i in dom f and A36: r1 = f . i and A37: r2 = f . (k + 1) ; ::_thesis: r1 <= r2 percases ( i < k + 1 or i >= k + 1 ) ; supposeA38: i < k + 1 ; ::_thesis: r1 <= r2 reconsider r3 = f . n1 as Real ; i <= k by A38, NAT_1:13; then r1 <= r3 by A5, A35, A36; hence r1 <= r2 by A24, A37, XXREAL_0:2; ::_thesis: verum end; suppose i >= k + 1 ; ::_thesis: r1 <= r2 hence r1 <= r2 by A34, A36, A37, XXREAL_0:1; ::_thesis: verum end; end; end; A39: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . (k + 1) holds k + 1 <= j proof let j be Element of NAT ; ::_thesis: ( j <= k + 1 & j in dom f & f . j = f . (k + 1) implies k + 1 <= j ) assume that j <= k + 1 and A40: ( j in dom f & f . j = f . (k + 1) ) ; ::_thesis: k + 1 <= j percases ( j < k + 1 or j >= k + 1 ) ; suppose j < k + 1 ; ::_thesis: k + 1 <= j then j <= k by NAT_1:13; hence k + 1 <= j by A5, A24, A40; ::_thesis: verum end; suppose j >= k + 1 ; ::_thesis: k + 1 <= j hence k + 1 <= j ; ::_thesis: verum end; end; end; 1 <= 1 + k by NAT_1:12; then ( k + 1 <> 0 implies ( k + 1 <= k + 1 & k + 1 in dom f ) ) by A1, A32, FINSEQ_1:1; hence S1[k + 1] by A33, A39; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; end; end; ( ( for i being Element of NAT for r1, r2 being Real st i <= 0 & i in dom f & r1 = f . i & r2 = f . 1 holds r1 <= r2 ) & ( for j being Element of NAT st j <= 0 & j in dom f & f . j = f . 1 holds 1 <= j ) ) by A1, FINSEQ_1:1; then A41: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A41, A3); then consider n1 being Element of NAT such that A42: ( len f <> 0 implies ( n1 <= len f & n1 in dom f ) ) and A43: for i being Element of NAT for r1, r2 being Real st i <= len f & i in dom f & r1 = f . i & r2 = f . n1 holds r1 <= r2 and A44: for j being Element of NAT st j <= len f & j in dom f & f . j = f . n1 holds n1 <= j ; A45: for j being Element of NAT st j in dom f & f . j = f . n1 holds n1 <= j proof let j be Element of NAT ; ::_thesis: ( j in dom f & f . j = f . n1 implies n1 <= j ) assume that A46: j in dom f and A47: f . j = f . n1 ; ::_thesis: n1 <= j j <= len f by A46, FINSEQ_3:25; hence n1 <= j by A44, A46, A47; ::_thesis: verum end; for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . n1 holds r1 <= r2 proof let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . n1 holds r1 <= r2 let r1, r2 be Real; ::_thesis: ( i in dom f & r1 = f . i & r2 = f . n1 implies r1 <= r2 ) assume that A48: i in dom f and A49: ( r1 = f . i & r2 = f . n1 ) ; ::_thesis: r1 <= r2 i <= len f by A48, FINSEQ_3:25; hence r1 <= r2 by A43, A48, A49; ::_thesis: verum end; hence ex b1 being Element of NAT st ( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds b1 <= j ) ) ) ) by A2, A42, A45; ::_thesis: verum end; end; end; uniqueness for b1, b2 being Element of NAT st ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds b1 <= j ) ) ) & ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b2 holds b2 <= j ) ) ) holds b1 = b2 proof thus for m1, m2 being Element of NAT st ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m1 holds m1 <= j ) ) ) & ( len f = 0 implies m2 = 0 ) & ( len f > 0 implies ( m2 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds m2 <= j ) ) ) holds m1 = m2 ::_thesis: verum proof let m1, m2 be Element of NAT ; ::_thesis: ( ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m1 holds m1 <= j ) ) ) & ( len f = 0 implies m2 = 0 ) & ( len f > 0 implies ( m2 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds m2 <= j ) ) ) implies m1 = m2 ) assume A50: ( ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m1 holds m1 <= j ) ) ) & ( len f = 0 implies m2 = 0 ) & ( len f > 0 implies ( m2 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds m2 <= j ) ) ) ) ; ::_thesis: m1 = m2 then ( f . m2 <= f . m1 & f . m1 <= f . m2 ) ; then f . m1 = f . m2 by XXREAL_0:1; then ( m1 <= m2 & m2 <= m1 ) by A50; hence m1 = m2 by XXREAL_0:1; ::_thesis: verum end; end; end; :: deftheorem Def1 defines max_p RFINSEQ2:def_1_:_ for f being FinSequence of REAL for b2 being Element of NAT holds ( b2 = max_p f iff ( ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds r1 <= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b2 holds b2 <= j ) ) ) ) ); definition let f be FinSequence of REAL ; func min_p f -> Element of NAT means :Def2: :: RFINSEQ2:def 2 ( ( len f = 0 implies it = 0 ) & ( len f > 0 implies ( it in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . it holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . it holds it <= j ) ) ) ); existence ex b1 being Element of NAT st ( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds b1 <= j ) ) ) ) proof A1: dom f = Seg (len f) by FINSEQ_1:def_3; now__::_thesis:_(_(_len_f_=_0_&_ex_b1_being_Element_of_NAT_st_ (_(_len_f_=_0_implies_b1_=_0_)_&_(_len_f_>_0_implies_(_b1_in_dom_f_&_(_for_i_being_Element_of_NAT_ for_r1,_r2_being_Real_st_i_in_dom_f_&_r1_=_f_._i_&_r2_=_f_._b1_holds_ r1_>=_r2_)_&_(_for_j_being_Element_of_NAT_st_j_in_dom_f_&_f_._j_=_f_._b1_holds_ b1_<=_j_)_)_)_)_)_or_(_len_f_<>_0_&_ex_b1_being_Element_of_NAT_st_ (_(_len_f_=_0_implies_b1_=_0_)_&_(_len_f_>_0_implies_(_b1_in_dom_f_&_(_for_i_being_Element_of_NAT_ for_r1,_r2_being_Real_st_i_in_dom_f_&_r1_=_f_._i_&_r2_=_f_._b1_holds_ r1_>=_r2_)_&_(_for_j_being_Element_of_NAT_st_j_in_dom_f_&_f_._j_=_f_._b1_holds_ b1_<=_j_)_)_)_)_)_) percases ( len f = 0 or len f <> 0 ) ; case len f = 0 ; ::_thesis: ex b1 being Element of NAT st ( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds b1 <= j ) ) ) ) hence ex b1 being Element of NAT st ( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds b1 <= j ) ) ) ) ; ::_thesis: verum end; caseA2: len f <> 0 ; ::_thesis: ex b1 being Element of NAT st ( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds b1 <= j ) ) ) ) defpred S1[ Element of NAT ] means ex n being Element of NAT st ( ( $1 <> 0 implies ( n <= $1 & n in dom f ) ) & ( for i being Element of NAT for r1, r2 being Real st i <= $1 & i in dom f & r1 = f . i & r2 = f . n holds r1 >= r2 ) & ( for j being Element of NAT st j <= $1 & j in dom f & f . j = f . n holds n <= j ) ); A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then consider n1 being Element of NAT such that A4: ( k <> 0 implies ( n1 <= k & n1 in dom f ) ) and A5: for i being Element of NAT for r1, r2 being Real st i <= k & i in dom f & r1 = f . i & r2 = f . n1 holds r1 >= r2 and A6: for j being Element of NAT st j <= k & j in dom f & f . j = f . n1 holds n1 <= j ; now__::_thesis:_(_(_k_=_0_&_S1[k_+_1]_)_or_(_k_<>_0_&_S1[k_+_1]_)_) percases ( k = 0 or k <> 0 ) ; caseA7: k = 0 ; ::_thesis: S1[k + 1] A8: dom f = Seg (len f) by FINSEQ_1:def_3; A9: for i being Element of NAT for r1, r2 being Real st i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 holds r1 >= r2 proof let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 holds r1 >= r2 let r1, r2 be Real; ::_thesis: ( i <= 1 & i in dom f & r1 = f . i & r2 = f . 1 implies r1 >= r2 ) assume that A10: i <= 1 and A11: i in dom f and A12: ( r1 = f . i & r2 = f . 1 ) ; ::_thesis: r1 >= r2 1 <= i by A11, FINSEQ_3:25; hence r1 >= r2 by A10, A12, XXREAL_0:1; ::_thesis: verum end; len f >= 0 + 1 by A2, NAT_1:13; then A13: 1 in dom f by A8, FINSEQ_1:1; for j being Element of NAT st j <= 1 & j in dom f & f . j = f . 1 holds 1 <= j by A8, FINSEQ_1:1; hence S1[k + 1] by A7, A13, A9; ::_thesis: verum end; caseA14: k <> 0 ; ::_thesis: S1[k + 1] now__::_thesis:_(_(_f_._n1_<=_f_._(k_+_1)_&_S1[k_+_1]_)_or_(_f_._n1_>_f_._(k_+_1)_&_S1[k_+_1]_)_) percases ( f . n1 <= f . (k + 1) or f . n1 > f . (k + 1) ) ; caseA15: f . n1 <= f . (k + 1) ; ::_thesis: S1[k + 1] A16: for i being Element of NAT for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds r1 >= r2 proof let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds r1 >= r2 let r1, r2 be Real; ::_thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 implies r1 >= r2 ) assume that A17: i <= k + 1 and A18: i in dom f and A19: ( r1 = f . i & r2 = f . n1 ) ; ::_thesis: r1 >= r2 percases ( i < k + 1 or i >= k + 1 ) ; suppose i < k + 1 ; ::_thesis: r1 >= r2 then i <= k by NAT_1:13; hence r1 >= r2 by A5, A18, A19; ::_thesis: verum end; suppose i >= k + 1 ; ::_thesis: r1 >= r2 hence r1 >= r2 by A15, A17, A19, XXREAL_0:1; ::_thesis: verum end; end; end; A20: n1 <= k + 1 by A4, A14, NAT_1:13; A21: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . n1 holds n1 <= j proof let j be Element of NAT ; ::_thesis: ( j <= k + 1 & j in dom f & f . j = f . n1 implies n1 <= j ) assume that A22: j <= k + 1 and A23: ( j in dom f & f . j = f . n1 ) ; ::_thesis: n1 <= j percases ( j < k + 1 or j >= k + 1 ) ; suppose j < k + 1 ; ::_thesis: n1 <= j then j <= k by NAT_1:13; hence n1 <= j by A6, A23; ::_thesis: verum end; suppose j >= k + 1 ; ::_thesis: n1 <= j hence n1 <= j by A20, A22, XXREAL_0:1; ::_thesis: verum end; end; end; ( k + 1 <> 0 implies ( n1 <= k + 1 & n1 in dom f ) ) by A4, A14, NAT_1:13; hence S1[k + 1] by A16, A21; ::_thesis: verum end; caseA24: f . n1 > f . (k + 1) ; ::_thesis: S1[k + 1] now__::_thesis:_(_(_k_+_1_>_len_f_&_S1[k_+_1]_)_or_(_k_+_1_<=_len_f_&_S1[k_+_1]_)_) percases ( k + 1 > len f or k + 1 <= len f ) ; caseA25: k + 1 > len f ; ::_thesis: S1[k + 1] A26: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . n1 holds n1 <= j proof let j be Element of NAT ; ::_thesis: ( j <= k + 1 & j in dom f & f . j = f . n1 implies n1 <= j ) assume that j <= k + 1 and A27: ( j in dom f & f . j = f . n1 ) ; ::_thesis: n1 <= j percases ( j < k + 1 or j >= k + 1 ) ; suppose j < k + 1 ; ::_thesis: n1 <= j then j <= k by NAT_1:13; hence n1 <= j by A6, A27; ::_thesis: verum end; suppose j >= k + 1 ; ::_thesis: n1 <= j then k < j by NAT_1:13; hence n1 <= j by A4, A14, XXREAL_0:2; ::_thesis: verum end; end; end; A28: k >= len f by A25, NAT_1:13; A29: for i being Element of NAT for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds r1 >= r2 proof let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 holds r1 >= r2 let r1, r2 be Real; ::_thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . n1 implies r1 >= r2 ) assume that i <= k + 1 and A30: i in dom f and A31: ( r1 = f . i & r2 = f . n1 ) ; ::_thesis: r1 >= r2 i <= len f by A1, A30, FINSEQ_1:1; then i <= k by A28, XXREAL_0:2; hence r1 >= r2 by A5, A30, A31; ::_thesis: verum end; n1 <= len f by A1, A4, A14, FINSEQ_1:1; then ( k + 1 <> 0 implies ( n1 <= k + 1 & n1 in dom f ) ) by A4, A14, A25, XXREAL_0:2; hence S1[k + 1] by A29, A26; ::_thesis: verum end; caseA32: k + 1 <= len f ; ::_thesis: S1[k + 1] set n2 = k + 1; A33: for i being Element of NAT for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) holds r1 >= r2 proof let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) holds r1 >= r2 let r1, r2 be Real; ::_thesis: ( i <= k + 1 & i in dom f & r1 = f . i & r2 = f . (k + 1) implies r1 >= r2 ) assume that A34: i <= k + 1 and A35: i in dom f and A36: r1 = f . i and A37: r2 = f . (k + 1) ; ::_thesis: r1 >= r2 percases ( i < k + 1 or i >= k + 1 ) ; supposeA38: i < k + 1 ; ::_thesis: r1 >= r2 reconsider r3 = f . n1 as Real ; i <= k by A38, NAT_1:13; then r1 >= r3 by A5, A35, A36; hence r1 >= r2 by A24, A37, XXREAL_0:2; ::_thesis: verum end; suppose i >= k + 1 ; ::_thesis: r1 >= r2 hence r1 >= r2 by A34, A36, A37, XXREAL_0:1; ::_thesis: verum end; end; end; A39: for j being Element of NAT st j <= k + 1 & j in dom f & f . j = f . (k + 1) holds k + 1 <= j proof let j be Element of NAT ; ::_thesis: ( j <= k + 1 & j in dom f & f . j = f . (k + 1) implies k + 1 <= j ) assume that j <= k + 1 and A40: ( j in dom f & f . j = f . (k + 1) ) ; ::_thesis: k + 1 <= j percases ( j < k + 1 or j >= k + 1 ) ; suppose j < k + 1 ; ::_thesis: k + 1 <= j then j <= k by NAT_1:13; hence k + 1 <= j by A5, A24, A40; ::_thesis: verum end; suppose j >= k + 1 ; ::_thesis: k + 1 <= j hence k + 1 <= j ; ::_thesis: verum end; end; end; 1 <= 1 + k by NAT_1:12; then ( k + 1 <> 0 implies ( k + 1 <= k + 1 & k + 1 in dom f ) ) by A1, A32, FINSEQ_1:1; hence S1[k + 1] by A33, A39; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; ( ( for i being Element of NAT for r1, r2 being Real st i <= 0 & i in dom f & r1 = f . i & r2 = f . 1 holds r1 >= r2 ) & ( for j being Element of NAT st j <= 0 & j in dom f & f . j = f . 1 holds 1 <= j ) ) by A1, FINSEQ_1:1; then A41: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A41, A3); then consider n1 being Element of NAT such that A42: ( len f <> 0 implies ( n1 <= len f & n1 in dom f ) ) and A43: for i being Element of NAT for r1, r2 being Real st i <= len f & i in dom f & r1 = f . i & r2 = f . n1 holds r1 >= r2 and A44: for j being Element of NAT st j <= len f & j in dom f & f . j = f . n1 holds n1 <= j ; A45: for j being Element of NAT st j in dom f & f . j = f . n1 holds n1 <= j proof let j be Element of NAT ; ::_thesis: ( j in dom f & f . j = f . n1 implies n1 <= j ) assume that A46: j in dom f and A47: f . j = f . n1 ; ::_thesis: n1 <= j j <= len f by A46, FINSEQ_3:25; hence n1 <= j by A44, A46, A47; ::_thesis: verum end; for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . n1 holds r1 >= r2 proof let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . n1 holds r1 >= r2 let r1, r2 be Real; ::_thesis: ( i in dom f & r1 = f . i & r2 = f . n1 implies r1 >= r2 ) assume that A48: i in dom f and A49: ( r1 = f . i & r2 = f . n1 ) ; ::_thesis: r1 >= r2 i <= len f by A48, FINSEQ_3:25; hence r1 >= r2 by A43, A48, A49; ::_thesis: verum end; hence ex b1 being Element of NAT st ( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds b1 <= j ) ) ) ) by A2, A42, A45; ::_thesis: verum end; end; end; hence ex b1 being Element of NAT st ( ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds b1 <= j ) ) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of NAT st ( len f = 0 implies b1 = 0 ) & ( len f > 0 implies ( b1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b1 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b1 holds b1 <= j ) ) ) & ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b2 holds b2 <= j ) ) ) holds b1 = b2 proof thus for m1, m2 being Element of NAT st ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m1 holds m1 <= j ) ) ) & ( len f = 0 implies m2 = 0 ) & ( len f > 0 implies ( m2 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds m2 <= j ) ) ) holds m1 = m2 ::_thesis: verum proof let m1, m2 be Element of NAT ; ::_thesis: ( ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m1 holds m1 <= j ) ) ) & ( len f = 0 implies m2 = 0 ) & ( len f > 0 implies ( m2 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds m2 <= j ) ) ) implies m1 = m2 ) assume A50: ( ( len f = 0 implies m1 = 0 ) & ( len f > 0 implies ( m1 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m1 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m1 holds m1 <= j ) ) ) & ( len f = 0 implies m2 = 0 ) & ( len f > 0 implies ( m2 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . m2 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . m2 holds m2 <= j ) ) ) ) ; ::_thesis: m1 = m2 then ( f . m2 >= f . m1 & f . m1 >= f . m2 ) ; then f . m1 = f . m2 by XXREAL_0:1; then ( m1 >= m2 & m2 >= m1 ) by A50; hence m1 = m2 by XXREAL_0:1; ::_thesis: verum end; end; end; :: deftheorem Def2 defines min_p RFINSEQ2:def_2_:_ for f being FinSequence of REAL for b2 being Element of NAT holds ( b2 = min_p f iff ( ( len f = 0 implies b2 = 0 ) & ( len f > 0 implies ( b2 in dom f & ( for i being Element of NAT for r1, r2 being Real st i in dom f & r1 = f . i & r2 = f . b2 holds r1 >= r2 ) & ( for j being Element of NAT st j in dom f & f . j = f . b2 holds b2 <= j ) ) ) ) ); definition let f be FinSequence of REAL ; func max f -> Real equals :: RFINSEQ2:def 3 f . (max_p f); correctness coherence f . (max_p f) is Real; ; func min f -> Real equals :: RFINSEQ2:def 4 f . (min_p f); correctness coherence f . (min_p f) is Real; ; end; :: deftheorem defines max RFINSEQ2:def_3_:_ for f being FinSequence of REAL holds max f = f . (max_p f); :: deftheorem defines min RFINSEQ2:def_4_:_ for f being FinSequence of REAL holds min f = f . (min_p f); theorem Th1: :: RFINSEQ2:1 for f being FinSequence of REAL for i being Element of NAT st 1 <= i & i <= len f holds ( f . i <= f . (max_p f) & f . i <= max f ) proof let f be FinSequence of REAL ; ::_thesis: for i being Element of NAT st 1 <= i & i <= len f holds ( f . i <= f . (max_p f) & f . i <= max f ) let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len f implies ( f . i <= f . (max_p f) & f . i <= max f ) ) assume A1: ( 1 <= i & i <= len f ) ; ::_thesis: ( f . i <= f . (max_p f) & f . i <= max f ) then A2: i in dom f by FINSEQ_3:25; hence f . i <= f . (max_p f) by A1, Def1; ::_thesis: f . i <= max f thus f . i <= max f by A1, A2, Def1; ::_thesis: verum end; theorem Th2: :: RFINSEQ2:2 for f being FinSequence of REAL for i being Element of NAT st 1 <= i & i <= len f holds ( f . i >= f . (min_p f) & f . i >= min f ) proof let f be FinSequence of REAL ; ::_thesis: for i being Element of NAT st 1 <= i & i <= len f holds ( f . i >= f . (min_p f) & f . i >= min f ) let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len f implies ( f . i >= f . (min_p f) & f . i >= min f ) ) assume A1: ( 1 <= i & i <= len f ) ; ::_thesis: ( f . i >= f . (min_p f) & f . i >= min f ) then A2: i in dom f by FINSEQ_3:25; hence f . i >= f . (min_p f) by A1, Def2; ::_thesis: f . i >= min f thus f . i >= min f by A1, A2, Def2; ::_thesis: verum end; theorem :: RFINSEQ2:3 for f being FinSequence of REAL for r being Real st f = <*r*> holds ( max_p f = 1 & max f = r ) proof let f be FinSequence of REAL ; ::_thesis: for r being Real st f = <*r*> holds ( max_p f = 1 & max f = r ) let r be Real; ::_thesis: ( f = <*r*> implies ( max_p f = 1 & max f = r ) ) assume A1: f = <*r*> ; ::_thesis: ( max_p f = 1 & max f = r ) then A2: f . 1 = r by FINSEQ_1:40; A3: len f = 1 by A1, FINSEQ_1:40; then max_p f in dom f by Def1; then ( 1 <= max_p f & max_p f <= len f ) by FINSEQ_3:25; hence ( max_p f = 1 & max f = r ) by A3, A2, XXREAL_0:1; ::_thesis: verum end; theorem :: RFINSEQ2:4 for f being FinSequence of REAL for r being Real st f = <*r*> holds ( min_p f = 1 & min f = r ) proof let f be FinSequence of REAL ; ::_thesis: for r being Real st f = <*r*> holds ( min_p f = 1 & min f = r ) let r be Real; ::_thesis: ( f = <*r*> implies ( min_p f = 1 & min f = r ) ) assume A1: f = <*r*> ; ::_thesis: ( min_p f = 1 & min f = r ) then A2: f . 1 = r by FINSEQ_1:40; A3: len f = 1 by A1, FINSEQ_1:40; then min_p f in dom f by Def2; then ( 1 <= min_p f & min_p f <= len f ) by FINSEQ_3:25; hence ( min_p f = 1 & min f = r ) by A3, A2, XXREAL_0:1; ::_thesis: verum end; theorem :: RFINSEQ2:5 for f being FinSequence of REAL for r1, r2 being Real st f = <*r1,r2*> holds ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) proof let f be FinSequence of REAL ; ::_thesis: for r1, r2 being Real st f = <*r1,r2*> holds ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) let r1, r2 be Real; ::_thesis: ( f = <*r1,r2*> implies ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) ) assume A1: f = <*r1,r2*> ; ::_thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) then A2: len f = 2 by FINSEQ_1:44; then A3: f . 2 <= f . (max_p f) by Th1; A4: f . 1 = r1 by A1, FINSEQ_1:44; A5: max_p f in dom f by A2, Def1; then A6: 1 <= max_p f by FINSEQ_3:25; A7: max_p f <= len f by A5, FINSEQ_3:25; A8: f . 2 = r2 by A1, FINSEQ_1:44; A9: f . 1 <= f . (max_p f) by A2, Th1; now__::_thesis:_(_(_r1_>=_r2_&_max_f_=_max_(r1,r2)_&_max_p_f_=_IFEQ_(r1,(max_(r1,r2)),1,2)_)_or_(_r1_<_r2_&_max_f_=_max_(r1,r2)_&_max_p_f_=_IFEQ_(r1,(max_(r1,r2)),1,2)_)_) percases ( r1 >= r2 or r1 < r2 ) ; case r1 >= r2 ; ::_thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) then A10: max (r1,r2) <= max f by A4, A9, XXREAL_0:def_10; now__::_thesis:_(_(_max_p_f_<_len_f_&_max_f_=_max_(r1,r2)_&_max_p_f_=_IFEQ_(r1,(max_(r1,r2)),1,2)_)_or_(_max_p_f_>=_len_f_&_max_f_=_max_(r1,r2)_&_max_p_f_=_IFEQ_(r1,(max_(r1,r2)),1,2)_)_) percases ( max_p f < len f or max_p f >= len f ) ; case max_p f < len f ; ::_thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) then max_p f < 1 + 1 by A1, FINSEQ_1:44; then max_p f <= 1 by NAT_1:13; then A11: max_p f = 1 by A6, XXREAL_0:1; then max f <= max (r1,r2) by A4, XXREAL_0:25; then max f = max (r1,r2) by A10, XXREAL_0:1; hence ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) by A4, A11, FUNCOP_1:def_8; ::_thesis: verum end; case max_p f >= len f ; ::_thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) then A12: max_p f = 2 by A2, A7, XXREAL_0:1; then max f <= max (r1,r2) by A8, XXREAL_0:25; then A13: max f = max (r1,r2) by A10, XXREAL_0:1; 1 in dom f by A2, FINSEQ_3:25; then r1 <> r2 by A2, A4, A8, A12, Def1; hence ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) by A8, A12, A13, FUNCOP_1:def_8; ::_thesis: verum end; end; end; hence ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) ; ::_thesis: verum end; case r1 < r2 ; ::_thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) then A14: max (r1,r2) <= max f by A8, A3, XXREAL_0:def_10; now__::_thesis:_(_(_max_p_f_<_len_f_&_max_f_=_max_(r1,r2)_&_max_p_f_=_IFEQ_(r1,(max_(r1,r2)),1,2)_)_or_(_max_p_f_>=_len_f_&_max_f_=_max_(r1,r2)_&_max_p_f_=_IFEQ_(r1,(max_(r1,r2)),1,2)_)_) percases ( max_p f < len f or max_p f >= len f ) ; case max_p f < len f ; ::_thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) then max_p f < 1 + 1 by A1, FINSEQ_1:44; then max_p f <= 1 by NAT_1:13; then A15: max_p f = 1 by A6, XXREAL_0:1; then max f <= max (r1,r2) by A4, XXREAL_0:25; then max f = max (r1,r2) by A14, XXREAL_0:1; hence ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) by A4, A15, FUNCOP_1:def_8; ::_thesis: verum end; case max_p f >= len f ; ::_thesis: ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) then A16: max_p f = 2 by A2, A7, XXREAL_0:1; then max f <= max (r1,r2) by A8, XXREAL_0:25; then A17: max f = max (r1,r2) by A14, XXREAL_0:1; 1 in dom f by A2, FINSEQ_3:25; then r1 <> r2 by A2, A4, A8, A16, Def1; hence ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) by A8, A16, A17, FUNCOP_1:def_8; ::_thesis: verum end; end; end; hence ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) ; ::_thesis: verum end; end; end; hence ( max f = max (r1,r2) & max_p f = IFEQ (r1,(max (r1,r2)),1,2) ) ; ::_thesis: verum end; theorem :: RFINSEQ2:6 for f being FinSequence of REAL for r1, r2 being Real st f = <*r1,r2*> holds ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) proof let f be FinSequence of REAL ; ::_thesis: for r1, r2 being Real st f = <*r1,r2*> holds ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) let r1, r2 be Real; ::_thesis: ( f = <*r1,r2*> implies ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) ) assume A1: f = <*r1,r2*> ; ::_thesis: ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) then A2: len f = 2 by FINSEQ_1:44; then A3: f . 1 >= f . (min_p f) by Th2; A4: f . 2 = r2 by A1, FINSEQ_1:44; A5: min_p f in dom f by A2, Def2; then A6: 1 <= min_p f by FINSEQ_3:25; A7: f . 2 >= f . (min_p f) by A2, Th2; A8: f . 1 = r1 by A1, FINSEQ_1:44; A9: min_p f <= len f by A5, FINSEQ_3:25; percases ( r1 <= r2 or r1 > r2 ) ; suppose r1 <= r2 ; ::_thesis: ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) then A10: min (r1,r2) >= min f by A8, A3, XXREAL_0:def_9; now__::_thesis:_(_(_min_p_f_<_len_f_&_min_f_=_min_(r1,r2)_&_min_p_f_=_IFEQ_(r1,(min_(r1,r2)),1,2)_)_or_(_min_p_f_>=_len_f_&_min_f_=_min_(r1,r2)_&_min_p_f_=_IFEQ_(r1,(min_(r1,r2)),1,2)_)_) percases ( min_p f < len f or min_p f >= len f ) ; case min_p f < len f ; ::_thesis: ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) then min_p f < 1 + 1 by A1, FINSEQ_1:44; then min_p f <= 1 by NAT_1:13; then A11: min_p f = 1 by A6, XXREAL_0:1; then min f >= min (r1,r2) by A8, XXREAL_0:17; then min f = min (r1,r2) by A10, XXREAL_0:1; hence ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) by A8, A11, FUNCOP_1:def_8; ::_thesis: verum end; case min_p f >= len f ; ::_thesis: ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) then A12: min_p f = 2 by A2, A9, XXREAL_0:1; then min f >= min (r1,r2) by A4, XXREAL_0:17; then A13: min f = min (r1,r2) by A10, XXREAL_0:1; 1 in dom f by A2, FINSEQ_3:25; then r1 <> r2 by A2, A8, A4, A12, Def2; hence ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) by A4, A12, A13, FUNCOP_1:def_8; ::_thesis: verum end; end; end; hence ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) ; ::_thesis: verum end; suppose r1 > r2 ; ::_thesis: ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) then A14: min (r1,r2) >= min f by A4, A7, XXREAL_0:def_9; now__::_thesis:_(_(_min_p_f_<_len_f_&_min_f_=_min_(r1,r2)_&_min_p_f_=_IFEQ_(r1,(min_(r1,r2)),1,2)_)_or_(_min_p_f_>=_len_f_&_min_f_=_min_(r1,r2)_&_min_p_f_=_IFEQ_(r1,(min_(r1,r2)),1,2)_)_) percases ( min_p f < len f or min_p f >= len f ) ; case min_p f < len f ; ::_thesis: ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) then min_p f < 1 + 1 by A1, FINSEQ_1:44; then min_p f <= 1 by NAT_1:13; then A15: min_p f = 1 by A6, XXREAL_0:1; then min f >= min (r1,r2) by A8, XXREAL_0:17; then min f = min (r1,r2) by A14, XXREAL_0:1; hence ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) by A8, A15, FUNCOP_1:def_8; ::_thesis: verum end; case min_p f >= len f ; ::_thesis: ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) then A16: min_p f = 2 by A2, A9, XXREAL_0:1; then min f >= min (r1,r2) by A4, XXREAL_0:17; then A17: min f = min (r1,r2) by A14, XXREAL_0:1; 1 in dom f by A2, FINSEQ_3:25; then r1 <> r2 by A2, A8, A4, A16, Def2; hence ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) by A4, A16, A17, FUNCOP_1:def_8; ::_thesis: verum end; end; end; hence ( min f = min (r1,r2) & min_p f = IFEQ (r1,(min (r1,r2)),1,2) ) ; ::_thesis: verum end; end; end; theorem :: RFINSEQ2:7 for f1, f2 being FinSequence of REAL st len f1 = len f2 & len f1 > 0 holds max (f1 + f2) <= (max f1) + (max f2) proof let f1, f2 be FinSequence of REAL ; ::_thesis: ( len f1 = len f2 & len f1 > 0 implies max (f1 + f2) <= (max f1) + (max f2) ) assume that A1: len f1 = len f2 and A2: len f1 > 0 ; ::_thesis: max (f1 + f2) <= (max f1) + (max f2) A3: len (f1 + f2) = len f1 by A1, RVSUM_1:115; then A4: max_p (f1 + f2) in dom (f1 + f2) by A2, Def1; then ( 1 <= max_p (f1 + f2) & max_p (f1 + f2) <= len (f1 + f2) ) by FINSEQ_3:25; then A5: max_p (f1 + f2) in Seg (len f1) by A3, FINSEQ_1:1; then max_p (f1 + f2) in dom f2 by A1, FINSEQ_1:def_3; then A6: f2 . (max_p (f1 + f2)) <= f2 . (max_p f2) by A1, A2, Def1; max_p (f1 + f2) in dom f1 by A5, FINSEQ_1:def_3; then A7: f1 . (max_p (f1 + f2)) <= f1 . (max_p f1) by A2, Def1; max (f1 + f2) = (f1 . (max_p (f1 + f2))) + (f2 . (max_p (f1 + f2))) by A4, VALUED_1:def_1; hence max (f1 + f2) <= (max f1) + (max f2) by A7, A6, XREAL_1:7; ::_thesis: verum end; theorem :: RFINSEQ2:8 for f1, f2 being FinSequence of REAL st len f1 = len f2 & len f1 > 0 holds min (f1 + f2) >= (min f1) + (min f2) proof let f1, f2 be FinSequence of REAL ; ::_thesis: ( len f1 = len f2 & len f1 > 0 implies min (f1 + f2) >= (min f1) + (min f2) ) assume that A1: len f1 = len f2 and A2: len f1 > 0 ; ::_thesis: min (f1 + f2) >= (min f1) + (min f2) A3: len (f1 + f2) = len f1 by A1, RVSUM_1:115; then A4: min_p (f1 + f2) in dom (f1 + f2) by A2, Def2; then ( 1 <= min_p (f1 + f2) & min_p (f1 + f2) <= len (f1 + f2) ) by FINSEQ_3:25; then A5: min_p (f1 + f2) in Seg (len f1) by A3, FINSEQ_1:1; then min_p (f1 + f2) in dom f2 by A1, FINSEQ_1:def_3; then A6: f2 . (min_p (f1 + f2)) >= f2 . (min_p f2) by A1, A2, Def2; min_p (f1 + f2) in dom f1 by A5, FINSEQ_1:def_3; then A7: f1 . (min_p (f1 + f2)) >= f1 . (min_p f1) by A2, Def2; min (f1 + f2) = (f1 . (min_p (f1 + f2))) + (f2 . (min_p (f1 + f2))) by A4, VALUED_1:def_1; hence min (f1 + f2) >= (min f1) + (min f2) by A7, A6, XREAL_1:7; ::_thesis: verum end; theorem :: RFINSEQ2:9 for f being FinSequence of REAL for a being Real st len f > 0 & a > 0 holds ( max (a * f) = a * (max f) & max_p (a * f) = max_p f ) proof let f be FinSequence of REAL ; ::_thesis: for a being Real st len f > 0 & a > 0 holds ( max (a * f) = a * (max f) & max_p (a * f) = max_p f ) let a be Real; ::_thesis: ( len f > 0 & a > 0 implies ( max (a * f) = a * (max f) & max_p (a * f) = max_p f ) ) assume that A1: len f > 0 and A2: a > 0 ; ::_thesis: ( max (a * f) = a * (max f) & max_p (a * f) = max_p f ) A3: len (a * f) = len f by RVSUM_1:117; then A4: max_p (a * f) in dom (a * f) by A1, Def1; then ( 1 <= max_p (a * f) & max_p (a * f) <= len (a * f) ) by FINSEQ_3:25; then max_p (a * f) in Seg (len f) by A3, FINSEQ_1:1; then A5: max_p (a * f) in dom f by FINSEQ_1:def_3; then f . (max_p f) >= f . (max_p (a * f)) by A1, Def1; then A6: a * (f . (max_p f)) >= a * (f . (max_p (a * f))) by A2, XREAL_1:64; A7: ( a * (f . (max_p f)) = (a * f) . (max_p f) & a * (f . (max_p (a * f))) = (a * f) . (max_p (a * f)) ) by RVSUM_1:44; A8: dom (a * f) = dom f by VALUED_1:def_5; then A9: max_p f in dom (a * f) by A1, Def1; then (a * f) . (max_p f) <= (a * f) . (max_p (a * f)) by A1, A3, Def1; then A10: f . (max_p f) <= f . (max_p (a * f)) by A2, A7, XREAL_1:68; f . (max_p (a * f)) <= f . (max_p f) by A1, A5, Def1; then f . (max_p f) = f . (max_p (a * f)) by A10, XXREAL_0:1; then A11: ( max (a * f) = a * (f . (max_p (a * f))) & max_p (a * f) >= max_p f ) by A1, A8, A4, Def1, RVSUM_1:44; max_p f in dom (a * f) by A1, A8, Def1; then (a * f) . (max_p (a * f)) >= (a * f) . (max_p f) by A1, A3, Def1; then (a * f) . (max_p (a * f)) = (a * f) . (max_p f) by A7, A6, XXREAL_0:1; then max_p (a * f) <= max_p f by A1, A3, A9, Def1; hence ( max (a * f) = a * (max f) & max_p (a * f) = max_p f ) by A11, XXREAL_0:1; ::_thesis: verum end; theorem :: RFINSEQ2:10 for f being FinSequence of REAL for a being Real st len f > 0 & a > 0 holds ( min (a * f) = a * (min f) & min_p (a * f) = min_p f ) proof let f be FinSequence of REAL ; ::_thesis: for a being Real st len f > 0 & a > 0 holds ( min (a * f) = a * (min f) & min_p (a * f) = min_p f ) let a be Real; ::_thesis: ( len f > 0 & a > 0 implies ( min (a * f) = a * (min f) & min_p (a * f) = min_p f ) ) assume that A1: len f > 0 and A2: a > 0 ; ::_thesis: ( min (a * f) = a * (min f) & min_p (a * f) = min_p f ) A3: len (a * f) = len f by RVSUM_1:117; then A4: min_p (a * f) in dom (a * f) by A1, Def2; then ( 1 <= min_p (a * f) & min_p (a * f) <= len (a * f) ) by FINSEQ_3:25; then A5: min_p (a * f) in dom f by A3, FINSEQ_3:25; then f . (min_p f) <= f . (min_p (a * f)) by A1, Def2; then A6: a * (f . (min_p f)) <= a * (f . (min_p (a * f))) by A2, XREAL_1:64; A7: ( a * (f . (min_p f)) = (a * f) . (min_p f) & a * (f . (min_p (a * f))) = (a * f) . (min_p (a * f)) ) by RVSUM_1:44; A8: dom (a * f) = dom f by VALUED_1:def_5; then A9: min_p f in dom (a * f) by A1, Def2; then (a * f) . (min_p f) >= (a * f) . (min_p (a * f)) by A1, A3, Def2; then A10: f . (min_p f) >= f . (min_p (a * f)) by A2, A7, XREAL_1:68; f . (min_p (a * f)) >= f . (min_p f) by A1, A5, Def2; then f . (min_p f) = f . (min_p (a * f)) by A10, XXREAL_0:1; then A11: ( min (a * f) = a * (f . (min_p (a * f))) & min_p (a * f) >= min_p f ) by A1, A8, A4, Def2, RVSUM_1:44; min_p f in dom (a * f) by A1, A8, Def2; then (a * f) . (min_p (a * f)) <= (a * f) . (min_p f) by A1, A3, Def2; then (a * f) . (min_p (a * f)) = (a * f) . (min_p f) by A7, A6, XXREAL_0:1; then min_p (a * f) <= min_p f by A1, A3, A9, Def2; hence ( min (a * f) = a * (min f) & min_p (a * f) = min_p f ) by A11, XXREAL_0:1; ::_thesis: verum end; theorem :: RFINSEQ2:11 for f being FinSequence of REAL st len f > 0 holds ( max (- f) = - (min f) & max_p (- f) = min_p f ) proof let f be FinSequence of REAL ; ::_thesis: ( len f > 0 implies ( max (- f) = - (min f) & max_p (- f) = min_p f ) ) assume A1: len f > 0 ; ::_thesis: ( max (- f) = - (min f) & max_p (- f) = min_p f ) A2: len (- f) = len f by RVSUM_1:114; then A3: max_p (- f) in dom (- f) by A1, Def1; then ( 1 <= max_p (- f) & max_p (- f) <= len (- f) ) by FINSEQ_3:25; then max_p (- f) in Seg (len f) by A2, FINSEQ_1:1; then A4: max_p (- f) in dom f by FINSEQ_1:def_3; then f . (min_p f) <= f . (max_p (- f)) by A1, Def2; then A5: - (f . (min_p f)) >= - (f . (max_p (- f))) by XREAL_1:24; A6: ( - (f . (min_p f)) = (- f) . (min_p f) & - (f . (max_p (- f))) = (- f) . (max_p (- f)) ) by RVSUM_1:17; A7: dom (- f) = dom f by VALUED_1:8; then A8: min_p f in dom (- f) by A1, Def2; then (- f) . (max_p (- f)) >= (- f) . (min_p f) by A1, A2, Def1; then A9: f . (max_p (- f)) <= f . (min_p f) by A6, XREAL_1:24; f . (min_p f) <= f . (max_p (- f)) by A1, A4, Def2; then f . (min_p f) = f . (max_p (- f)) by A9, XXREAL_0:1; then A10: ( max (- f) = - (f . (max_p (- f))) & max_p (- f) >= min_p f ) by A1, A7, A3, Def2, RVSUM_1:17; min_p f in dom (- f) by A1, A7, Def2; then (- f) . (max_p (- f)) >= (- f) . (min_p f) by A1, A2, Def1; then (- f) . (max_p (- f)) = (- f) . (min_p f) by A6, A5, XXREAL_0:1; then max_p (- f) <= min_p f by A1, A2, A8, Def1; hence ( max (- f) = - (min f) & max_p (- f) = min_p f ) by A10, XXREAL_0:1; ::_thesis: verum end; theorem :: RFINSEQ2:12 for f being FinSequence of REAL st len f > 0 holds ( min (- f) = - (max f) & min_p (- f) = max_p f ) proof let f be FinSequence of REAL ; ::_thesis: ( len f > 0 implies ( min (- f) = - (max f) & min_p (- f) = max_p f ) ) assume A1: len f > 0 ; ::_thesis: ( min (- f) = - (max f) & min_p (- f) = max_p f ) A2: len (- f) = len f by RVSUM_1:114; then A3: min_p (- f) in dom (- f) by A1, Def2; then ( 1 <= min_p (- f) & min_p (- f) <= len (- f) ) by FINSEQ_3:25; then min_p (- f) in Seg (len f) by A2, FINSEQ_1:1; then A4: min_p (- f) in dom f by FINSEQ_1:def_3; then f . (max_p f) >= f . (min_p (- f)) by A1, Def1; then A5: - (f . (max_p f)) <= - (f . (min_p (- f))) by XREAL_1:24; A6: ( - (f . (max_p f)) = (- f) . (max_p f) & - (f . (min_p (- f))) = (- f) . (min_p (- f)) ) by RVSUM_1:17; A7: dom (- f) = dom f by VALUED_1:8; then A8: max_p f in dom (- f) by A1, Def1; then (- f) . (min_p (- f)) <= (- f) . (max_p f) by A1, A2, Def2; then A9: f . (min_p (- f)) >= f . (max_p f) by A6, XREAL_1:24; f . (max_p f) >= f . (min_p (- f)) by A1, A4, Def1; then f . (max_p f) = f . (min_p (- f)) by A9, XXREAL_0:1; then A10: ( min (- f) = - (f . (min_p (- f))) & min_p (- f) >= max_p f ) by A1, A7, A3, Def1, RVSUM_1:17; max_p f in dom (- f) by A1, A7, Def1; then (- f) . (min_p (- f)) <= (- f) . (max_p f) by A1, A2, Def2; then (- f) . (min_p (- f)) = (- f) . (max_p f) by A6, A5, XXREAL_0:1; then min_p (- f) <= max_p f by A1, A2, A8, Def2; hence ( min (- f) = - (max f) & min_p (- f) = max_p f ) by A10, XXREAL_0:1; ::_thesis: verum end; theorem :: RFINSEQ2:13 for f being FinSequence of REAL for n being Element of NAT st n < len f holds ( max (f /^ n) <= max f & min (f /^ n) >= min f ) proof let f be FinSequence of REAL ; ::_thesis: for n being Element of NAT st n < len f holds ( max (f /^ n) <= max f & min (f /^ n) >= min f ) let n be Element of NAT ; ::_thesis: ( n < len f implies ( max (f /^ n) <= max f & min (f /^ n) >= min f ) ) A1: 1 <= 1 + n by NAT_1:12; assume A2: n < len f ; ::_thesis: ( max (f /^ n) <= max f & min (f /^ n) >= min f ) then A3: len (f /^ n) = (len f) - n by RFINSEQ:def_1; then A4: len (f /^ n) > 0 by A2, XREAL_1:50; then A5: min_p (f /^ n) in dom (f /^ n) by Def2; then A6: f . ((min_p (f /^ n)) + n) = min (f /^ n) by A2, RFINSEQ:def_1; min_p (f /^ n) <= len (f /^ n) by A5, FINSEQ_3:25; then A7: (min_p (f /^ n)) + n <= ((len f) - n) + n by A3, XREAL_1:7; A8: 1 <= 1 + n by NAT_1:12; 1 <= min_p (f /^ n) by A5, FINSEQ_3:25; then 1 + n <= (min_p (f /^ n)) + n by XREAL_1:7; then 1 <= (min_p (f /^ n)) + n by A8, XXREAL_0:2; then A9: (min_p (f /^ n)) + n in dom f by A7, FINSEQ_3:25; A10: max_p (f /^ n) in dom (f /^ n) by A4, Def1; then max_p (f /^ n) <= len (f /^ n) by FINSEQ_3:25; then A11: (max_p (f /^ n)) + n <= ((len f) - n) + n by A3, XREAL_1:7; 1 <= max_p (f /^ n) by A10, FINSEQ_3:25; then 1 + n <= (max_p (f /^ n)) + n by XREAL_1:7; then 1 <= (max_p (f /^ n)) + n by A1, XXREAL_0:2; then A12: (max_p (f /^ n)) + n in dom f by A11, FINSEQ_3:25; f . ((max_p (f /^ n)) + n) = max (f /^ n) by A2, A10, RFINSEQ:def_1; hence ( max (f /^ n) <= max f & min (f /^ n) >= min f ) by A2, A12, A9, A6, Def1, Def2; ::_thesis: verum end; Lm1: for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds max f <= max g proof let f, g be FinSequence of REAL ; ::_thesis: ( f,g are_fiberwise_equipotent implies max f <= max g ) assume A1: f,g are_fiberwise_equipotent ; ::_thesis: max f <= max g then consider P being Permutation of (dom g) such that A2: f = g * P by RFINSEQ:4; A3: dom f = dom g by A1, RFINSEQ:3; A4: len f = len g by A1, RFINSEQ:3; percases ( len f > 0 or len f <= 0 ) ; supposeA5: len f > 0 ; ::_thesis: max f <= max g then A6: max_p f in dom (g * P) by A2, Def1; then A7: (g * P) . (max_p f) = g . (P . (max_p f)) by FUNCT_1:12; dom g = Seg (len g) by FINSEQ_1:def_3; then dom P = dom g by A4, A5, FUNCT_2:def_1; then A8: ( rng P = dom g & P . (max_p f) in rng P ) by A2, A3, A6, FUNCT_1:def_3, FUNCT_2:def_3; then reconsider n = P . (max_p f) as Element of NAT ; dom g = Seg (len g) by FINSEQ_1:def_3; then ( 1 <= n & n <= len g ) by A8, FINSEQ_1:1; hence max f <= max g by A2, A7, Th1; ::_thesis: verum end; suppose len f <= 0 ; ::_thesis: max f <= max g then ( f = {} & g = {} ) by A4; hence max f <= max g ; ::_thesis: verum end; end; end; theorem Th14: :: RFINSEQ2:14 for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds max f = max g proof let f, g be FinSequence of REAL ; ::_thesis: ( f,g are_fiberwise_equipotent implies max f = max g ) assume f,g are_fiberwise_equipotent ; ::_thesis: max f = max g then ( max f <= max g & max g <= max f ) by Lm1; hence max f = max g by XXREAL_0:1; ::_thesis: verum end; Lm2: for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds min f >= min g proof let f, g be FinSequence of REAL ; ::_thesis: ( f,g are_fiberwise_equipotent implies min f >= min g ) assume A1: f,g are_fiberwise_equipotent ; ::_thesis: min f >= min g then consider P being Permutation of (dom g) such that A2: f = g * P by RFINSEQ:4; A3: len f = len g by A1, RFINSEQ:3; percases ( len f > 0 or len f <= 0 ) ; supposeA4: len f > 0 ; ::_thesis: min f >= min g dom g = Seg (len g) by FINSEQ_1:def_3; then A5: dom P = dom g by A3, A4, FUNCT_2:def_1; A6: min_p f in dom (g * P) by A2, A4, Def2; then A7: (g * P) . (min_p f) = g . (P . (min_p f)) by FUNCT_1:12; min_p f in dom g by A1, A2, A6, RFINSEQ:3; then A8: ( rng P = dom g & P . (min_p f) in rng P ) by A5, FUNCT_1:def_3, FUNCT_2:def_3; then reconsider n = P . (min_p f) as Element of NAT ; dom g = Seg (len g) by FINSEQ_1:def_3; then ( 1 <= n & n <= len g ) by A8, FINSEQ_1:1; hence min f >= min g by A2, A7, Th2; ::_thesis: verum end; suppose len f <= 0 ; ::_thesis: min f >= min g then ( f = {} & g = {} ) by A3; hence min f >= min g ; ::_thesis: verum end; end; end; theorem Th15: :: RFINSEQ2:15 for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds min f = min g proof let f, g be FinSequence of REAL ; ::_thesis: ( f,g are_fiberwise_equipotent implies min f = min g ) assume f,g are_fiberwise_equipotent ; ::_thesis: min f = min g then ( min f >= min g & min g >= min f ) by Lm2; hence min f = min g by XXREAL_0:1; ::_thesis: verum end; definition let f be FinSequence of REAL ; func sort_d f -> non-increasing FinSequence of REAL means :Def5: :: RFINSEQ2:def 5 f,it are_fiberwise_equipotent ; existence ex b1 being non-increasing FinSequence of REAL st f,b1 are_fiberwise_equipotent by RFINSEQ:22; uniqueness for b1, b2 being non-increasing FinSequence of REAL st f,b1 are_fiberwise_equipotent & f,b2 are_fiberwise_equipotent holds b1 = b2 by CLASSES1:76, RFINSEQ:23; projectivity for b1 being non-increasing FinSequence of REAL for b2 being FinSequence of REAL st b2,b1 are_fiberwise_equipotent holds b1,b1 are_fiberwise_equipotent ; end; :: deftheorem Def5 defines sort_d RFINSEQ2:def_5_:_ for f being FinSequence of REAL for b2 being non-increasing FinSequence of REAL holds ( b2 = sort_d f iff f,b2 are_fiberwise_equipotent ); theorem Th16: :: RFINSEQ2:16 for R being FinSequence of REAL st ( len R = 0 or len R = 1 ) holds R is non-decreasing proof let R be FinSequence of REAL ; ::_thesis: ( ( len R = 0 or len R = 1 ) implies R is non-decreasing ) assume A1: ( len R = 0 or len R = 1 ) ; ::_thesis: R is non-decreasing percases ( len R = 0 or len R = 1 ) by A1; suppose len R = 0 ; ::_thesis: R is non-decreasing then R = <*> REAL ; then for n being Element of NAT st n in dom R & n + 1 in dom R holds R . n <= R . (n + 1) ; hence R is non-decreasing by INTEGRA2:def_1; ::_thesis: verum end; suppose len R = 1 ; ::_thesis: R is non-decreasing then A2: dom R = {1} by FINSEQ_1:2, FINSEQ_1:def_3; now__::_thesis:_for_n_being_Element_of_NAT_st_n_in_dom_R_&_n_+_1_in_dom_R_holds_ R_._n_<=_R_._(n_+_1) let n be Element of NAT ; ::_thesis: ( n in dom R & n + 1 in dom R implies R . n <= R . (n + 1) ) assume that A3: n in dom R and A4: n + 1 in dom R ; ::_thesis: R . n <= R . (n + 1) n = 1 by A2, A3, TARSKI:def_1; hence R . n <= R . (n + 1) by A2, A4, TARSKI:def_1; ::_thesis: verum end; hence R is non-decreasing by INTEGRA2:def_1; ::_thesis: verum end; end; end; theorem Th17: :: RFINSEQ2:17 for R being FinSequence of REAL holds ( R is non-decreasing iff for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n <= R . m ) proof let R be FinSequence of REAL ; ::_thesis: ( R is non-decreasing iff for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n <= R . m ) thus ( R is non-decreasing implies for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n <= R . m ) ::_thesis: ( ( for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n <= R . m ) implies R is non-decreasing ) proof defpred S1[ Element of NAT ] means ( $1 in dom R implies for n being Element of NAT st n in dom R & n < $1 holds R . n <= R . $1 ); assume A1: R is non-decreasing ; ::_thesis: for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n <= R . m A2: for m being Element of NAT st S1[m] holds S1[m + 1] proof let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] ) assume A3: S1[m] ; ::_thesis: S1[m + 1] assume A4: m + 1 in dom R ; ::_thesis: for n being Element of NAT st n in dom R & n < m + 1 holds R . n <= R . (m + 1) then m + 1 <= len R by FINSEQ_3:25; then A5: m <= len R by NAT_1:13; let n be Element of NAT ; ::_thesis: ( n in dom R & n < m + 1 implies R . n <= R . (m + 1) ) assume that A6: n in dom R and A7: n < m + 1 ; ::_thesis: R . n <= R . (m + 1) set t = R . m; set r = R . n; set s = R . (m + 1); A8: n <= m by A7, NAT_1:13; 1 <= n by A6, FINSEQ_3:25; then A9: 1 <= m by A8, XXREAL_0:2; then A10: m in dom R by A5, FINSEQ_3:25; now__::_thesis:_(_(_n_=_m_&_R_._n_<=_R_._(m_+_1)_)_or_(_n_<>_m_&_R_._n_<=_R_._(m_+_1)_)_) percases ( n = m or n <> m ) ; case n = m ; ::_thesis: R . n <= R . (m + 1) hence R . n <= R . (m + 1) by A1, A4, A6, INTEGRA2:def_1; ::_thesis: verum end; case n <> m ; ::_thesis: R . n <= R . (m + 1) then n < m by A8, XXREAL_0:1; then A11: R . n <= R . m by A3, A6, A9, A5, FINSEQ_3:25; R . m <= R . (m + 1) by A1, A4, A10, INTEGRA2:def_1; hence R . n <= R . (m + 1) by A11, XXREAL_0:2; ::_thesis: verum end; end; end; hence R . n <= R . (m + 1) ; ::_thesis: verum end; A12: S1[ 0 ] ; for m being Element of NAT holds S1[m] from NAT_1:sch_1(A12, A2); hence for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n <= R . m ; ::_thesis: verum end; assume A13: for n, m being Element of NAT st n in dom R & m in dom R & n < m holds R . n <= R . m ; ::_thesis: R is non-decreasing let n be Element of NAT ; :: according to INTEGRA2:def_1 ::_thesis: ( not n in dom R or not n + 1 in dom R or R . n <= R . (n + 1) ) A14: n < n + 1 by NAT_1:13; assume ( n in dom R & n + 1 in dom R ) ; ::_thesis: R . n <= R . (n + 1) hence R . n <= R . (n + 1) by A13, A14; ::_thesis: verum end; Lm3: for f, g being non-decreasing FinSequence of REAL for n being Element of NAT st len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent holds ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent ) proof let f, g be non-decreasing FinSequence of REAL ; ::_thesis: for n being Element of NAT st len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent holds ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent ) let n be Element of NAT ; ::_thesis: ( len f = n + 1 & len f = len g & f,g are_fiberwise_equipotent implies ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent ) ) assume that A1: len f = n + 1 and A2: len f = len g and A3: f,g are_fiberwise_equipotent ; ::_thesis: ( f . (len f) = g . (len g) & f | n,g | n are_fiberwise_equipotent ) set r = f . (n + 1); set s = g . (n + 1); A4: 0 + 1 <= n + 1 by NAT_1:13; then A5: n + 1 in dom f by A1, FINSEQ_3:25; A6: f = (f | n) ^ <*(f . (n + 1))*> by A1, RFINSEQ:7; A7: n + 1 in dom g by A1, A2, A4, FINSEQ_3:25; A8: now__::_thesis:_not_f_._(n_+_1)_<>_g_._(n_+_1) A9: rng f = rng g by A3, CLASSES1:75; assume A10: f . (n + 1) <> g . (n + 1) ; ::_thesis: contradiction now__::_thesis:_(_(_f_._(n_+_1)_<_g_._(n_+_1)_&_contradiction_)_or_(_f_._(n_+_1)_>_g_._(n_+_1)_&_contradiction_)_) percases ( f . (n + 1) < g . (n + 1) or f . (n + 1) > g . (n + 1) ) by A10, XXREAL_0:1; caseA11: f . (n + 1) < g . (n + 1) ; ::_thesis: contradiction g . (n + 1) in rng f by A7, A9, FUNCT_1:def_3; then consider m being Nat such that A12: m in dom f and A13: f . m = g . (n + 1) by FINSEQ_2:10; A14: m <= len f by A12, FINSEQ_3:25; now__::_thesis:_(_(_m_=_len_f_&_contradiction_)_or_(_m_<>_len_f_&_contradiction_)_) percases ( m = len f or m <> len f ) ; case m = len f ; ::_thesis: contradiction hence contradiction by A1, A11, A13; ::_thesis: verum end; case m <> len f ; ::_thesis: contradiction then m < n + 1 by A1, A14, XXREAL_0:1; hence contradiction by A5, A11, A12, A13, Th17; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; caseA15: f . (n + 1) > g . (n + 1) ; ::_thesis: contradiction f . (n + 1) in rng g by A5, A9, FUNCT_1:def_3; then consider m being Nat such that A16: m in dom g and A17: g . m = f . (n + 1) by FINSEQ_2:10; A18: m <= len g by A16, FINSEQ_3:25; now__::_thesis:_(_(_m_=_len_g_&_contradiction_)_or_(_m_<>_len_g_&_contradiction_)_) percases ( m = len g or m <> len g ) ; case m = len g ; ::_thesis: contradiction hence contradiction by A1, A2, A15, A17; ::_thesis: verum end; case m <> len g ; ::_thesis: contradiction then m < n + 1 by A1, A2, A18, XXREAL_0:1; hence contradiction by A7, A15, A16, A17, Th17; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; hence f . (len f) = g . (len g) by A1, A2; ::_thesis: f | n,g | n are_fiberwise_equipotent A19: g = (g | n) ^ <*(f . (n + 1))*> by A1, A2, A8, RFINSEQ:7; now__::_thesis:_for_x_being_set_holds_card_(Coim_((f_|_n),x))_=_card_(Coim_((g_|_n),x)) let x be set ; ::_thesis: card (Coim ((f | n),x)) = card (Coim ((g | n),x)) (card ((f | n) " {x})) + (card (<*(f . (n + 1))*> " {x})) = card (Coim (f,x)) by A6, FINSEQ_3:57 .= card (Coim (g,x)) by A3, CLASSES1:def_9 .= (card ((g | n) " {x})) + (card (<*(f . (n + 1))*> " {x})) by A19, FINSEQ_3:57 ; hence card (Coim ((f | n),x)) = card (Coim ((g | n),x)) ; ::_thesis: verum end; hence f | n,g | n are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum end; theorem Th18: :: RFINSEQ2:18 for R being non-decreasing FinSequence of REAL for n being Element of NAT holds R | n is non-decreasing FinSequence of REAL proof let f be non-decreasing FinSequence of REAL ; ::_thesis: for n being Element of NAT holds f | n is non-decreasing FinSequence of REAL let n be Element of NAT ; ::_thesis: f | n is non-decreasing FinSequence of REAL set fn = f | n; now__::_thesis:_(_(_n_=_0_&_f_|_n_is_non-decreasing_FinSequence_of_REAL_)_or_(_n_<>_0_&_f_|_n_is_non-decreasing_FinSequence_of_REAL_)_) percases ( n = 0 or n <> 0 ) ; case n = 0 ; ::_thesis: f | n is non-decreasing FinSequence of REAL then len (f | n) = 0 ; hence f | n is non-decreasing FinSequence of REAL by Th16; ::_thesis: verum end; case n <> 0 ; ::_thesis: f | n is non-decreasing FinSequence of REAL then A1: 0 + 1 <= n by NAT_1:13; now__::_thesis:_(_(_len_f_<=_n_&_f_|_n_is_non-decreasing_FinSequence_of_REAL_)_or_(_n_<_len_f_&_f_|_n_is_non-decreasing_FinSequence_of_REAL_)_) percases ( len f <= n or n < len f ) ; case len f <= n ; ::_thesis: f | n is non-decreasing FinSequence of REAL hence f | n is non-decreasing FinSequence of REAL by FINSEQ_1:58; ::_thesis: verum end; case n < len f ; ::_thesis: f | n is non-decreasing FinSequence of REAL then A2: ( n in dom f & len (f | n) = n ) by A1, FINSEQ_1:59, FINSEQ_3:25; now__::_thesis:_for_m_being_Element_of_NAT_st_m_in_dom_(f_|_n)_&_m_+_1_in_dom_(f_|_n)_holds_ (f_|_n)_._m_<=_(f_|_n)_._(m_+_1) let m be Element of NAT ; ::_thesis: ( m in dom (f | n) & m + 1 in dom (f | n) implies (f | n) . m <= (f | n) . (m + 1) ) A3: dom (f | n) = Seg (len (f | n)) by FINSEQ_1:def_3; assume A4: ( m in dom (f | n) & m + 1 in dom (f | n) ) ; ::_thesis: (f | n) . m <= (f | n) . (m + 1) then A5: ( m in dom f & m + 1 in dom f ) by A2, A3, RFINSEQ:6; ( f . m = (f | n) . m & f . (m + 1) = (f | n) . (m + 1) ) by A2, A4, A3, RFINSEQ:6; hence (f | n) . m <= (f | n) . (m + 1) by A5, INTEGRA2:def_1; ::_thesis: verum end; hence f | n is non-decreasing FinSequence of REAL by INTEGRA2:def_1; ::_thesis: verum end; end; end; hence f | n is non-decreasing FinSequence of REAL ; ::_thesis: verum end; end; end; hence f | n is non-decreasing FinSequence of REAL ; ::_thesis: verum end; Lm4: for n being Element of NAT for g1, g2 being non-decreasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds g1 = g2 proof defpred S1[ Element of NAT ] means for g1, g2 being non-decreasing FinSequence of REAL st $1 = len g1 & g1,g2 are_fiberwise_equipotent holds g1 = g2; A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] let g1, g2 be non-decreasing FinSequence of REAL ; ::_thesis: ( n + 1 = len g1 & g1,g2 are_fiberwise_equipotent implies g1 = g2 ) set r = g1 . (n + 1); reconsider g1n = g1 | n, g2n = g2 | n as non-decreasing FinSequence of REAL by Th18; assume that A3: len g1 = n + 1 and A4: g1,g2 are_fiberwise_equipotent ; ::_thesis: g1 = g2 A5: len g2 = len g1 by A4, RFINSEQ:3; then A6: g1 . (len g1) = g2 . (len g2) by A3, A4, Lm3; A7: (g1 | n) ^ <*(g1 . (n + 1))*> = g1 by A3, RFINSEQ:7; len (g1 | n) = n by A3, FINSEQ_1:59, NAT_1:11; then g1n = g2n by A2, A3, A4, A5, Lm3; hence g1 = g2 by A3, A5, A6, A7, RFINSEQ:7; ::_thesis: verum end; A8: S1[ 0 ] proof let g1, g2 be non-decreasing FinSequence of REAL ; ::_thesis: ( 0 = len g1 & g1,g2 are_fiberwise_equipotent implies g1 = g2 ) assume ( len g1 = 0 & g1,g2 are_fiberwise_equipotent ) ; ::_thesis: g1 = g2 then ( len g2 = len g1 & g1 = <*> REAL ) by RFINSEQ:3; hence g1 = g2 ; ::_thesis: verum end; for m being Element of NAT holds S1[m] from NAT_1:sch_1(A8, A1); hence for n being Element of NAT for g1, g2 being non-decreasing FinSequence of REAL st n = len g1 & g1,g2 are_fiberwise_equipotent holds g1 = g2 ; ::_thesis: verum end; theorem Th19: :: RFINSEQ2:19 for R1, R2 being non-decreasing FinSequence of REAL st R1,R2 are_fiberwise_equipotent holds R1 = R2 proof let g1, g2 be non-decreasing FinSequence of REAL ; ::_thesis: ( g1,g2 are_fiberwise_equipotent implies g1 = g2 ) A1: len g1 = len g1 ; assume g1,g2 are_fiberwise_equipotent ; ::_thesis: g1 = g2 hence g1 = g2 by A1, Lm4; ::_thesis: verum end; definition let f be FinSequence of REAL ; func sort_a f -> non-decreasing FinSequence of REAL means :Def6: :: RFINSEQ2:def 6 f,it are_fiberwise_equipotent ; existence ex b1 being non-decreasing FinSequence of REAL st f,b1 are_fiberwise_equipotent by INTEGRA2:3; uniqueness for b1, b2 being non-decreasing FinSequence of REAL st f,b1 are_fiberwise_equipotent & f,b2 are_fiberwise_equipotent holds b1 = b2 by Th19, CLASSES1:76; projectivity for b1 being non-decreasing FinSequence of REAL for b2 being FinSequence of REAL st b2,b1 are_fiberwise_equipotent holds b1,b1 are_fiberwise_equipotent ; end; :: deftheorem Def6 defines sort_a RFINSEQ2:def_6_:_ for f being FinSequence of REAL for b2 being non-decreasing FinSequence of REAL holds ( b2 = sort_a f iff f,b2 are_fiberwise_equipotent ); theorem :: RFINSEQ2:20 for f being non-increasing FinSequence of REAL holds sort_d f = f by Def5; theorem :: RFINSEQ2:21 for f being non-decreasing FinSequence of REAL holds sort_a f = f by Def6; theorem :: RFINSEQ2:22 canceled; theorem :: RFINSEQ2:23 canceled; theorem Th24: :: RFINSEQ2:24 for f being FinSequence of REAL st f is non-increasing holds - f is non-decreasing proof let f be FinSequence of REAL ; ::_thesis: ( f is non-increasing implies - f is non-decreasing ) assume A1: f is non-increasing ; ::_thesis: - f is non-decreasing for n being Element of NAT st n in dom (- f) & n + 1 in dom (- f) holds (- f) . n <= (- f) . (n + 1) proof let n be Element of NAT ; ::_thesis: ( n in dom (- f) & n + 1 in dom (- f) implies (- f) . n <= (- f) . (n + 1) ) A2: dom (- f) = dom f by VALUED_1:8; A3: ( (- f) . n = - (f . n) & (- f) . (n + 1) = - (f . (n + 1)) ) by RVSUM_1:17; assume ( n in dom (- f) & n + 1 in dom (- f) ) ; ::_thesis: (- f) . n <= (- f) . (n + 1) then f . n >= f . (n + 1) by A1, A2, RFINSEQ:def_3; hence (- f) . n <= (- f) . (n + 1) by A3, XREAL_1:24; ::_thesis: verum end; hence - f is non-decreasing by INTEGRA2:def_1; ::_thesis: verum end; theorem Th25: :: RFINSEQ2:25 for f being FinSequence of REAL st f is non-decreasing holds - f is non-increasing proof let f be FinSequence of REAL ; ::_thesis: ( f is non-decreasing implies - f is non-increasing ) assume A1: f is non-decreasing ; ::_thesis: - f is non-increasing for n being Element of NAT st n in dom (- f) & n + 1 in dom (- f) holds (- f) . n >= (- f) . (n + 1) proof let n be Element of NAT ; ::_thesis: ( n in dom (- f) & n + 1 in dom (- f) implies (- f) . n >= (- f) . (n + 1) ) A2: dom (- f) = dom f by VALUED_1:8; A3: ( (- f) . n = - (f . n) & (- f) . (n + 1) = - (f . (n + 1)) ) by RVSUM_1:17; assume ( n in dom (- f) & n + 1 in dom (- f) ) ; ::_thesis: (- f) . n >= (- f) . (n + 1) then f . n <= f . (n + 1) by A1, A2, INTEGRA2:def_1; hence (- f) . n >= (- f) . (n + 1) by A3, XREAL_1:24; ::_thesis: verum end; hence - f is non-increasing by RFINSEQ:def_3; ::_thesis: verum end; theorem Th26: :: RFINSEQ2:26 for f, g being FinSequence of REAL for P being Permutation of (dom g) st f = g * P & len g >= 1 holds - f = (- g) * P proof let f, g be FinSequence of REAL ; ::_thesis: for P being Permutation of (dom g) st f = g * P & len g >= 1 holds - f = (- g) * P let P be Permutation of (dom g); ::_thesis: ( f = g * P & len g >= 1 implies - f = (- g) * P ) assume that A1: f = g * P and A2: len g >= 1 ; ::_thesis: - f = (- g) * P A3: rng P = dom g by FUNCT_2:def_3; A4: dom (- g) = dom g by VALUED_1:8; then A5: rng ((- g) * P) = rng (- g) by A3, RELAT_1:28; A6: dom (- f) = dom (g * P) by A1, VALUED_1:8; then A7: dom (- f) = dom P by A3, RELAT_1:27; then A8: dom (- f) = dom ((- g) * P) by A3, A4, RELAT_1:27; A9: dom g = Seg (len g) by FINSEQ_1:def_3; then dom P = dom g by A2, FUNCT_2:def_1; then (- g) * P is FinSequence by A9, A7, A8, FINSEQ_1:def_2; then reconsider k = (- g) * P as FinSequence of REAL by A5, FINSEQ_1:def_4; for i being Nat st i in dom (- f) holds (- f) . i = k . i proof let i be Nat; ::_thesis: ( i in dom (- f) implies (- f) . i = k . i ) assume A10: i in dom (- f) ; ::_thesis: (- f) . i = k . i then P . i in rng P by A7, FUNCT_1:3; then reconsider j = P . i as Element of NAT by A3; (- f) . i = - (f . i) by RVSUM_1:17 .= - (g . (P . i)) by A1, A6, A10, FUNCT_1:12 .= (- g) . j by RVSUM_1:17 .= ((- g) * P) . i by A8, A10, FUNCT_1:12 ; hence (- f) . i = k . i ; ::_thesis: verum end; hence - f = (- g) * P by A8, FINSEQ_1:13; ::_thesis: verum end; theorem Th27: :: RFINSEQ2:27 for f, g being FinSequence of REAL st f,g are_fiberwise_equipotent holds - f, - g are_fiberwise_equipotent proof let f, g be FinSequence of REAL ; ::_thesis: ( f,g are_fiberwise_equipotent implies - f, - g are_fiberwise_equipotent ) assume A1: f,g are_fiberwise_equipotent ; ::_thesis: - f, - g are_fiberwise_equipotent then consider P being Permutation of (dom g) such that A2: f = g * P by RFINSEQ:4; A3: now__::_thesis:_(_(_len_g_>=_1_&_-_f_=_(-_g)_*_P_)_or_(_len_g_<_1_&_-_f_=_(-_g)_*_P_)_) percases ( len g >= 1 or len g < 1 ) ; case len g >= 1 ; ::_thesis: - f = (- g) * P hence - f = (- g) * P by A2, Th26; ::_thesis: verum end; case len g < 1 ; ::_thesis: - f = (- g) * P then A4: len g < 0 + 1 ; then A5: g = {} by NAT_1:13; len g = 0 by A4, NAT_1:13; then A6: len f = 0 by A1, RFINSEQ:3; then len (- f) = 0 by RVSUM_1:114; then A7: - f = {} ; f = {} by A6; hence - f = (- g) * P by A2, A5, A7; ::_thesis: verum end; end; end; dom (- g) = dom g by VALUED_1:8; hence - f, - g are_fiberwise_equipotent by A3, RFINSEQ:4; ::_thesis: verum end; theorem :: RFINSEQ2:28 for f being FinSequence of REAL holds sort_d (- f) = - (sort_a f) proof let f be FinSequence of REAL ; ::_thesis: sort_d (- f) = - (sort_a f) - f, sort_d (- f) are_fiberwise_equipotent by Def5; then A1: - (- f), - (sort_d (- f)) are_fiberwise_equipotent by Th27; - (sort_d (- f)) is non-decreasing by Th24; then - (sort_d (- f)) = sort_a f by A1, Def6; hence sort_d (- f) = - (sort_a f) ; ::_thesis: verum end; theorem :: RFINSEQ2:29 for f being FinSequence of REAL holds sort_a (- f) = - (sort_d f) proof let f be FinSequence of REAL ; ::_thesis: sort_a (- f) = - (sort_d f) - f, sort_a (- f) are_fiberwise_equipotent by Def6; then A1: - (- f), - (sort_a (- f)) are_fiberwise_equipotent by Th27; - (sort_a (- f)) is non-increasing by Th25; then - (sort_a (- f)) = sort_d f by A1, Def5; hence sort_a (- f) = - (sort_d f) ; ::_thesis: verum end; theorem Th30: :: RFINSEQ2:30 for f being FinSequence of REAL holds ( dom (sort_d f) = dom f & len (sort_d f) = len f ) proof let f be FinSequence of REAL ; ::_thesis: ( dom (sort_d f) = dom f & len (sort_d f) = len f ) f, sort_d f are_fiberwise_equipotent by Def5; hence ( dom (sort_d f) = dom f & len (sort_d f) = len f ) by RFINSEQ:3; ::_thesis: verum end; theorem Th31: :: RFINSEQ2:31 for f being FinSequence of REAL holds ( dom (sort_a f) = dom f & len (sort_a f) = len f ) proof let f be FinSequence of REAL ; ::_thesis: ( dom (sort_a f) = dom f & len (sort_a f) = len f ) f, sort_a f are_fiberwise_equipotent by Def6; hence ( dom (sort_a f) = dom f & len (sort_a f) = len f ) by RFINSEQ:3; ::_thesis: verum end; theorem :: RFINSEQ2:32 for f being FinSequence of REAL st len f >= 1 holds ( max_p (sort_d f) = 1 & min_p (sort_a f) = 1 & (sort_d f) . 1 = max f & (sort_a f) . 1 = min f ) proof let f be FinSequence of REAL ; ::_thesis: ( len f >= 1 implies ( max_p (sort_d f) = 1 & min_p (sort_a f) = 1 & (sort_d f) . 1 = max f & (sort_a f) . 1 = min f ) ) assume A1: len f >= 1 ; ::_thesis: ( max_p (sort_d f) = 1 & min_p (sort_a f) = 1 & (sort_d f) . 1 = max f & (sort_a f) . 1 = min f ) A2: len (sort_d f) = len f by Th30; then 1 in Seg (len (sort_d f)) by A1, FINSEQ_1:1; then A3: 1 in dom (sort_d f) by FINSEQ_1:def_3; A4: for i being Element of NAT for r1, r2 being Real st i in dom (sort_d f) & r1 = (sort_d f) . i & r2 = (sort_d f) . 1 holds r1 <= r2 proof let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i in dom (sort_d f) & r1 = (sort_d f) . i & r2 = (sort_d f) . 1 holds r1 <= r2 let r1, r2 be Real; ::_thesis: ( i in dom (sort_d f) & r1 = (sort_d f) . i & r2 = (sort_d f) . 1 implies r1 <= r2 ) assume that A5: i in dom (sort_d f) and A6: ( r1 = (sort_d f) . i & r2 = (sort_d f) . 1 ) ; ::_thesis: r1 <= r2 i in Seg (len (sort_d f)) by A5, FINSEQ_1:def_3; then A7: 1 <= i by FINSEQ_1:1; now__::_thesis:_(_(_1_=_i_&_r1_<=_r2_)_or_(_1_<>_i_&_r1_<=_r2_)_) percases ( 1 = i or 1 <> i ) ; case 1 = i ; ::_thesis: r1 <= r2 hence r1 <= r2 by A6; ::_thesis: verum end; case 1 <> i ; ::_thesis: r1 <= r2 then 1 < i by A7, XXREAL_0:1; hence r1 <= r2 by A3, A5, A6, RFINSEQ:19; ::_thesis: verum end; end; end; hence r1 <= r2 ; ::_thesis: verum end; A8: len (sort_a f) = len f by Th31; then A9: 1 in dom (sort_a f) by A1, FINSEQ_3:25; A10: for i being Element of NAT for r1, r2 being Real st i in dom (sort_a f) & r1 = (sort_a f) . i & r2 = (sort_a f) . 1 holds r1 >= r2 proof let i be Element of NAT ; ::_thesis: for r1, r2 being Real st i in dom (sort_a f) & r1 = (sort_a f) . i & r2 = (sort_a f) . 1 holds r1 >= r2 let r1, r2 be Real; ::_thesis: ( i in dom (sort_a f) & r1 = (sort_a f) . i & r2 = (sort_a f) . 1 implies r1 >= r2 ) assume that A11: i in dom (sort_a f) and A12: ( r1 = (sort_a f) . i & r2 = (sort_a f) . 1 ) ; ::_thesis: r1 >= r2 A13: 1 <= i by A11, FINSEQ_3:25; percases ( 1 = i or 1 <> i ) ; suppose 1 = i ; ::_thesis: r1 >= r2 hence r1 >= r2 by A12; ::_thesis: verum end; suppose 1 <> i ; ::_thesis: r1 >= r2 then 1 < i by A13, XXREAL_0:1; hence r1 >= r2 by A9, A11, A12, Th17; ::_thesis: verum end; end; end; A14: f, sort_a f are_fiberwise_equipotent by Def6; A15: f, sort_d f are_fiberwise_equipotent by Def5; A16: for j being Element of NAT st j in dom (sort_a f) & (sort_a f) . j = (sort_a f) . 1 holds 1 <= j by FINSEQ_3:25; then A17: (sort_a f) . 1 = min (sort_a f) by A1, A8, A9, A10, Def2 .= min f by A14, Th15 ; A18: for j being Element of NAT st j in dom (sort_d f) & (sort_d f) . j = (sort_d f) . 1 holds 1 <= j proof let j be Element of NAT ; ::_thesis: ( j in dom (sort_d f) & (sort_d f) . j = (sort_d f) . 1 implies 1 <= j ) assume that A19: j in dom (sort_d f) and (sort_d f) . j = (sort_d f) . 1 ; ::_thesis: 1 <= j j in Seg (len (sort_d f)) by A19, FINSEQ_1:def_3; hence 1 <= j by FINSEQ_1:1; ::_thesis: verum end; then (sort_d f) . 1 = max (sort_d f) by A1, A2, A3, A4, Def1 .= max f by A15, Th14 ; hence ( max_p (sort_d f) = 1 & min_p (sort_a f) = 1 & (sort_d f) . 1 = max f & (sort_a f) . 1 = min f ) by A1, A2, A3, A4, A18, A8, A9, A10, A16, A17, Def1, Def2; ::_thesis: verum end;