:: MESFUNC3 semantic presentation begin theorem Th1: :: MESFUNC3:1 for n, m being Nat for a being Function of [:(Seg n),(Seg m):],REAL for p, q being FinSequence of REAL st dom p = Seg n & ( for i being Nat st i in dom p holds ex r being FinSequence of REAL st ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds ex s being FinSequence of REAL st ( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,j] ) ) ) holds Sum p = Sum q proof defpred S1[ Nat] means for m being Nat for a being Function of [:(Seg \$1),(Seg m):],REAL for p, q being FinSequence of REAL st dom p = Seg \$1 & ( for i being Nat st i in dom p holds ex r being FinSequence of REAL st ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds ex s being FinSequence of REAL st ( dom s = Seg \$1 & q . j = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,j] ) ) ) holds Sum p = Sum q; A1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] reconsider n = n as Element of NAT by ORDINAL1:def_12; now__::_thesis:_for_m_being_Nat for_a_being_Function_of_[:(Seg_(n_+_1)),(Seg_m):],REAL for_p,_q_being_FinSequence_of_REAL_st_dom_p_=_Seg_(n_+_1)_&_(_for_i_being_Nat_st_i_in_dom_p_holds_ ex_r_being_FinSequence_of_REAL_st_ (_dom_r_=_Seg_m_&_p_._i_=_Sum_r_&_(_for_j_being_Nat_st_j_in_dom_r_holds_ r_._j_=_a_._[i,j]_)_)_)_&_dom_q_=_Seg_m_&_(_for_j_being_Nat_st_j_in_dom_q_holds_ ex_s_being_FinSequence_of_REAL_st_ (_dom_s_=_Seg_(n_+_1)_&_q_._j_=_Sum_s_&_(_for_i_being_Nat_st_i_in_dom_s_holds_ s_._i_=_a_._[i,j]_)_)_)_holds_ Sum_p_=_Sum_q let m be Nat; ::_thesis: for a being Function of [:(Seg (n + 1)),(Seg m):],REAL for p, q being FinSequence of REAL st dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds ex r being FinSequence of REAL st ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds ex s being FinSequence of REAL st ( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,j] ) ) ) holds Sum p = Sum q let a be Function of [:(Seg (n + 1)),(Seg m):],REAL; ::_thesis: for p, q being FinSequence of REAL st dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds ex r being FinSequence of REAL st ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds ex s being FinSequence of REAL st ( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,j] ) ) ) holds Sum p = Sum q let p, q be FinSequence of REAL ; ::_thesis: ( dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds ex r being FinSequence of REAL st ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds ex s being FinSequence of REAL st ( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,j] ) ) ) implies Sum p = Sum q ) assume that A3: dom p = Seg (n + 1) and A4: for i being Nat st i in dom p holds ex r being FinSequence of REAL st ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) and A5: dom q = Seg m and A6: for j being Nat st j in dom q holds ex s being FinSequence of REAL st ( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,j] ) ) ; ::_thesis: Sum p = Sum q set a0 = a | [:(Seg n),(Seg m):]; n <= n + 1 by NAT_1:11; then Seg n c= Seg (n + 1) by FINSEQ_1:5; then [:(Seg n),(Seg m):] c= [:(Seg (n + 1)),(Seg m):] by ZFMISC_1:95; then reconsider a0 = a | [:(Seg n),(Seg m):] as Function of [:(Seg n),(Seg m):],REAL by FUNCT_2:32; deffunc H1( Nat) -> Element of REAL = a . [(n + 1),\$1]; reconsider p0 = p | (Seg n) as FinSequence of REAL by FINSEQ_1:18; len p = n + 1 by A3, FINSEQ_1:def_3; then A7: n <= len p by NAT_1:11; then A8: dom p0 = Seg n by FINSEQ_1:17; A9: dom p0 = Seg n by A7, FINSEQ_1:17; A10: now__::_thesis:_for_i_being_Nat_st_i_in_dom_p0_holds_ ex_r_being_FinSequence_of_REAL_st_ (_dom_r_=_Seg_m_&_p0_._i_=_Sum_r_&_(_for_j_being_Nat_st_j_in_dom_r_holds_ r_._j_=_a0_._[i,j]_)_) let i be Nat; ::_thesis: ( i in dom p0 implies ex r being FinSequence of REAL st ( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds r . j = a0 . [i,j] ) ) ) assume A11: i in dom p0 ; ::_thesis: ex r being FinSequence of REAL st ( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds r . j = a0 . [i,j] ) ) consider r being FinSequence of REAL such that A12: dom r = Seg m and A13: p . i = Sum r and A14: for j being Nat st j in dom r holds r . j = a . [i,j] by A3, A4, A9, A11, FINSEQ_2:8; take r = r; ::_thesis: ( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds r . j = a0 . [i,j] ) ) thus dom r = Seg m by A12; ::_thesis: ( p0 . i = Sum r & ( for j being Nat st j in dom r holds r . j = a0 . [i,j] ) ) thus p0 . i = Sum r by A11, A13, FUNCT_1:47; ::_thesis: for j being Nat st j in dom r holds r . j = a0 . [i,j] thus for j being Nat st j in dom r holds r . j = a0 . [i,j] ::_thesis: verum proof n <= n + 1 by NAT_1:11; then A15: Seg n c= Seg (n + 1) by FINSEQ_1:5; dom a = [:(Seg (n + 1)),(Seg m):] by FUNCT_2:def_1; then A16: dom a0 = [:(Seg (n + 1)),(Seg m):] /\ [:(Seg n),(Seg m):] by RELAT_1:61 .= [:(Seg n),(Seg m):] by A15, ZFMISC_1:101 ; let j be Nat; ::_thesis: ( j in dom r implies r . j = a0 . [i,j] ) assume A17: j in dom r ; ::_thesis: r . j = a0 . [i,j] A18: [i,j] in [:(Seg n),(Seg m):] by A9, A11, A12, A17, ZFMISC_1:87; thus r . j = a . [i,j] by A14, A17 .= a0 . [i,j] by A18, A16, FUNCT_1:47 ; ::_thesis: verum end; end; reconsider m = m as Element of NAT by ORDINAL1:def_12; consider an being FinSequence such that A19: ( len an = m & ( for j being Nat st j in dom an holds an . j = H1(j) ) ) from FINSEQ_1:sch_2(); A20: now__::_thesis:_for_i_being_Nat_st_i_in_dom_an_holds_ an_._i_in_REAL let i be Nat; ::_thesis: ( i in dom an implies an . i in REAL ) assume i in dom an ; ::_thesis: an . i in REAL then an . i = a . [(n + 1),i] by A19; hence an . i in REAL ; ::_thesis: verum end; A21: dom an = Seg m by A19, FINSEQ_1:def_3; reconsider an = an as FinSequence of REAL by A20, FINSEQ_2:12; A22: an is Element of m -tuples_on REAL by A19, FINSEQ_2:92; A23: dom an = Seg m by A19, FINSEQ_1:def_3; A24: Sum an = p . (n + 1) proof consider r being FinSequence of REAL such that A25: dom r = Seg m and A26: p . (n + 1) = Sum r and A27: for j being Nat st j in dom r holds r . j = a . [(n + 1),j] by A3, A4, FINSEQ_1:4; now__::_thesis:_for_j_being_Nat_st_j_in_dom_r_holds_ r_._j_=_an_._j let j be Nat; ::_thesis: ( j in dom r implies r . j = an . j ) assume A28: j in dom r ; ::_thesis: r . j = an . j hence r . j = a . [(n + 1),j] by A27 .= an . j by A19, A21, A25, A28 ; ::_thesis: verum end; hence Sum an = p . (n + 1) by A23, A25, A26, FINSEQ_1:13; ::_thesis: verum end; reconsider q0 = q - an as FinSequence of REAL ; A29: rng <:q,an:> c= [:(rng q),(rng an):] by FUNCT_3:51; dom diffreal = [:REAL,REAL:] by FUNCT_2:def_1; then A30: [:(rng q),(rng an):] c= dom diffreal by ZFMISC_1:96; dom (diffreal .: (q,an)) = dom (diffreal * <:q,an:>) by FUNCOP_1:def_3 .= dom <:q,an:> by A30, A29, RELAT_1:27, XBOOLE_1:1 .= (dom q) /\ (dom an) by FUNCT_3:def_7 ; then A31: dom q0 = (dom q) /\ (dom an) by RVSUM_1:def_6 .= (Seg m) /\ (Seg m) by A5, A19, FINSEQ_1:def_3 .= Seg m ; then len q0 = m by FINSEQ_1:def_3; then A32: q0 is Element of m -tuples_on REAL by FINSEQ_2:92; A33: now__::_thesis:_for_j_being_Nat_st_j_in_dom_q0_holds_ ex_sn_being_FinSequence_of_REAL_st_ (_dom_sn_=_Seg_n_&_q0_._j_=_Sum_sn_&_(_for_i_being_Nat_st_i_in_dom_sn_holds_ sn_._i_=_a0_._[i,j]_)_) let j be Nat; ::_thesis: ( j in dom q0 implies ex sn being FinSequence of REAL st ( dom sn = Seg n & q0 . j = Sum sn & ( for i being Nat st i in dom sn holds sn . i = a0 . [i,j] ) ) ) assume A34: j in dom q0 ; ::_thesis: ex sn being FinSequence of REAL st ( dom sn = Seg n & q0 . j = Sum sn & ( for i being Nat st i in dom sn holds sn . i = a0 . [i,j] ) ) consider s being FinSequence of REAL such that A35: dom s = Seg (n + 1) and A36: q . j = Sum s and A37: for i being Nat st i in dom s holds s . i = a . [i,j] by A5, A6, A31, A34; s . (n + 1) = a . [(n + 1),j] by A35, A37, FINSEQ_1:4; then A38: s . (n + 1) = an . j by A19, A21, A31, A34; reconsider sn = s | (Seg n) as FinSequence of REAL by FINSEQ_1:18; take sn = sn; ::_thesis: ( dom sn = Seg n & q0 . j = Sum sn & ( for i being Nat st i in dom sn holds sn . i = a0 . [i,j] ) ) A39: len s = n + 1 by A35, FINSEQ_1:def_3; then n <= len s by NAT_1:11; hence A40: dom sn = Seg n by FINSEQ_1:17; ::_thesis: ( q0 . j = Sum sn & ( for i being Nat st i in dom sn holds sn . i = a0 . [i,j] ) ) sn ^ <*(s . (n + 1))*> = s by A39, FINSEQ_3:55; then (q . j) - (an . j) = ((Sum sn) + (an . j)) - (an . j) by A36, A38, RVSUM_1:74 .= Sum sn ; hence q0 . j = Sum sn by A34, VALUED_1:13; ::_thesis: for i being Nat st i in dom sn holds sn . i = a0 . [i,j] thus for i being Nat st i in dom sn holds sn . i = a0 . [i,j] ::_thesis: verum proof n <= n + 1 by NAT_1:11; then A41: Seg n c= Seg (n + 1) by FINSEQ_1:5; dom a = [:(Seg (n + 1)),(Seg m):] by FUNCT_2:def_1; then A42: dom a0 = [:(Seg (n + 1)),(Seg m):] /\ [:(Seg n),(Seg m):] by RELAT_1:61 .= [:(Seg n),(Seg m):] by A41, ZFMISC_1:101 ; let i be Nat; ::_thesis: ( i in dom sn implies sn . i = a0 . [i,j] ) assume A43: i in dom sn ; ::_thesis: sn . i = a0 . [i,j] A44: [i,j] in [:(Seg n),(Seg m):] by A31, A34, A40, A43, ZFMISC_1:87; thus sn . i = s . i by A43, FUNCT_1:47 .= a . [i,j] by A35, A37, A40, A43, A41 .= a0 . [i,j] by A44, A42, FUNCT_1:47 ; ::_thesis: verum end; end; len q = m by A5, FINSEQ_1:def_3; then q is Element of m -tuples_on REAL by FINSEQ_2:92; then A45: q0 + an = q by A22, RVSUM_1:43; len p = n + 1 by A3, FINSEQ_1:def_3; then p0 ^ <*(Sum an)*> = p by A24, FINSEQ_3:55; hence Sum p = (Sum p0) + (Sum an) by RVSUM_1:74 .= (Sum q0) + (Sum an) by A2, A10, A8, A31, A33 .= Sum q by A32, A22, A45, RVSUM_1:89 ; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; now__::_thesis:_for_m_being_Nat for_a_being_Function_of_[:(Seg_0),(Seg_m):],REAL for_p,_q_being_FinSequence_of_REAL_st_dom_p_=_Seg_0_&_(_for_i_being_Nat_st_i_in_dom_p_holds_ ex_r_being_FinSequence_of_REAL_st_ (_dom_r_=_Seg_m_&_p_._i_=_Sum_r_&_(_for_j_being_Nat_st_j_in_dom_r_holds_ r_._j_=_a_._[i,j]_)_)_)_&_dom_q_=_Seg_m_&_(_for_j_being_Nat_st_j_in_dom_q_holds_ ex_s_being_FinSequence_of_REAL_st_ (_dom_s_=_Seg_0_&_q_._j_=_Sum_s_&_(_for_i_being_Nat_st_i_in_dom_s_holds_ s_._i_=_a_._[i,j]_)_)_)_holds_ Sum_p_=_Sum_q let m be Nat; ::_thesis: for a being Function of [:(Seg 0),(Seg m):],REAL for p, q being FinSequence of REAL st dom p = Seg 0 & ( for i being Nat st i in dom p holds ex r being FinSequence of REAL st ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds ex s being FinSequence of REAL st ( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,j] ) ) ) holds Sum p = Sum q let a be Function of [:(Seg 0),(Seg m):],REAL; ::_thesis: for p, q being FinSequence of REAL st dom p = Seg 0 & ( for i being Nat st i in dom p holds ex r being FinSequence of REAL st ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds ex s being FinSequence of REAL st ( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,j] ) ) ) holds Sum p = Sum q let p, q be FinSequence of REAL ; ::_thesis: ( dom p = Seg 0 & ( for i being Nat st i in dom p holds ex r being FinSequence of REAL st ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds ex s being FinSequence of REAL st ( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,j] ) ) ) implies Sum p = Sum q ) assume that A46: dom p = Seg 0 and for i being Nat st i in dom p holds ex r being FinSequence of REAL st ( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) and A47: dom q = Seg m and A48: for j being Nat st j in dom q holds ex s being FinSequence of REAL st ( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,j] ) ) ; ::_thesis: Sum p = Sum q reconsider m = m as Element of NAT by ORDINAL1:def_12; now__::_thesis:_for_z_being_set_st_z_in_dom_q_holds_ q_._z_=_0 let z be set ; ::_thesis: ( z in dom q implies q . z = 0 ) assume A49: z in dom q ; ::_thesis: q . z = 0 then z in { k where k is Element of NAT : ( 1 <= k & k <= m ) } by A47, FINSEQ_1:def_1; then ex k being Element of NAT st ( z = k & 1 <= k & k <= m ) ; then reconsider j = z as Nat ; consider s being FinSequence of REAL such that A50: dom s = Seg 0 and A51: q . j = Sum s and for i being Nat st i in dom s holds s . i = a . [i,j] by A48, A49; s = <*> REAL by A50; hence q . z = 0 by A51, RVSUM_1:72; ::_thesis: verum end; then q = (dom q) --> 0 by FUNCOP_1:11; then A52: q = m |-> 0 by A47, FINSEQ_2:def_2; p = <*> REAL by A46; hence Sum p = Sum q by A52, RVSUM_1:72, RVSUM_1:81; ::_thesis: verum end; then A53: S1[ 0 ] ; thus for n being Nat holds S1[n] from NAT_1:sch_2(A53, A1); ::_thesis: verum end; theorem Th2: :: MESFUNC3:2 for F being FinSequence of ExtREAL for f being FinSequence of REAL st F = f holds Sum F = Sum f proof let F be FinSequence of ExtREAL ; ::_thesis: for f being FinSequence of REAL st F = f holds Sum F = Sum f let f be FinSequence of REAL ; ::_thesis: ( F = f implies Sum F = Sum f ) defpred S1[ Nat] means for G being FinSequence of ExtREAL for g being FinSequence of REAL st G = F | (Seg \$1) & g = f | (Seg \$1) & \$1 <= len F holds Sum G = Sum g; F | (Seg (len F)) = F | (len F) by FINSEQ_1:def_15; then A1: F | (Seg (len F)) = F by FINSEQ_1:58; assume A2: F = f ; ::_thesis: Sum F = Sum f A3: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] for G being FinSequence of ExtREAL for g being FinSequence of REAL st G = F | (Seg (k + 1)) & g = f | (Seg (k + 1)) & k + 1 <= len F holds Sum G = Sum g proof let G be FinSequence of ExtREAL ; ::_thesis: for g being FinSequence of REAL st G = F | (Seg (k + 1)) & g = f | (Seg (k + 1)) & k + 1 <= len F holds Sum G = Sum g let g be FinSequence of REAL ; ::_thesis: ( G = F | (Seg (k + 1)) & g = f | (Seg (k + 1)) & k + 1 <= len F implies Sum G = Sum g ) assume that A5: G = F | (Seg (k + 1)) and A6: g = f | (Seg (k + 1)) and A7: k + 1 <= len F ; ::_thesis: Sum G = Sum g reconsider g2 = <*(g . (k + 1))*> as FinSequence of REAL ; reconsider G1 = G | (Seg k) as FinSequence of ExtREAL by FINSEQ_1:18; A8: now__::_thesis:_(_not_-infty_in_rng_G1_&_not_-infty_in_rng_<*(G_._(k_+_1))*>_) A9: rng g2 c= REAL ; assume ( -infty in rng G1 or -infty in rng <*(G . (k + 1))*> ) ; ::_thesis: contradiction hence contradiction by A2, A5, A6, A9; ::_thesis: verum end; reconsider g1 = g | (Seg k) as FinSequence of REAL by FINSEQ_1:18; len g = k + 1 by A2, A6, A7, FINSEQ_1:17; then g = g1 ^ <*(g . (k + 1))*> by FINSEQ_3:55; then A10: Sum g = (Sum g1) + (g . (k + 1)) by RVSUM_1:74; A11: k <= k + 1 by NAT_1:11; len G = k + 1 by A5, A7, FINSEQ_1:17; then G = G1 ^ <*(G . (k + 1))*> by FINSEQ_3:55; then A12: Sum G = (Sum G1) + (Sum <*(G . (k + 1))*>) by A8, EXTREAL1:10 .= (Sum G1) + (G . (k + 1)) by EXTREAL1:8 ; k <= k + 1 by NAT_1:11; then Seg k c= Seg (k + 1) by FINSEQ_1:5; then ( G1 = F | (Seg k) & g1 = f | (Seg k) ) by A5, A6, FUNCT_1:51; then Sum G1 = Sum g1 by A4, A7, A11, XXREAL_0:2; hence Sum G = Sum g by A2, A5, A6, A12, A10, SUPINF_2:1; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A13: S1[ 0 ] by EXTREAL1:7, RVSUM_1:72; for k being Nat holds S1[k] from NAT_1:sch_2(A13, A3); hence Sum F = Sum f by A2, A1; ::_thesis: verum end; theorem Th3: :: MESFUNC3:3 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & ( for x being set st x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & ( for x being set st x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & ( for x being set st x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) ) let f be PartFunc of X,ExtREAL; ::_thesis: ( f is_simple_func_in S implies ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & ( for x being set st x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) ) ) assume f is_simple_func_in S ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & ( for x being set st x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) ) then consider F being Finite_Sep_Sequence of S such that A1: dom f = union (rng F) and A2: for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y by MESFUNC2:def_4; defpred S1[ Nat, Element of ExtREAL ] means for x being set st x in F . \$1 holds \$2 = f . x; A3: for k being Nat st k in Seg (len F) holds ex y being Element of ExtREAL st S1[k,y] proof let k be Nat; ::_thesis: ( k in Seg (len F) implies ex y being Element of ExtREAL st S1[k,y] ) assume k in Seg (len F) ; ::_thesis: ex y being Element of ExtREAL st S1[k,y] then A4: k in dom F by FINSEQ_1:def_3; then A5: F . k in rng F by FUNCT_1:3; now__::_thesis:_(_(_F_._k_=_{}_&_ex_y_being_Element_of_ExtREAL_ex_y_being_Element_of_ExtREAL_st_S1[k,y]_)_or_(_F_._k_<>_{}_&_ex_y_being_Element_of_ExtREAL_ex_y_being_Element_of_ExtREAL_st_S1[k,y]_)_) percases ( F . k = {} or F . k <> {} ) ; caseA6: F . k = {} ; ::_thesis: ex y being Element of ExtREAL ex y being Element of ExtREAL st S1[k,y] take y = 0. ; ::_thesis: ex y being Element of ExtREAL st S1[k,y] for x being set st x in F . k holds y = f . x by A6; hence ex y being Element of ExtREAL st S1[k,y] ; ::_thesis: verum end; case F . k <> {} ; ::_thesis: ex y being Element of ExtREAL ex y being Element of ExtREAL st S1[k,y] then consider x1 being set such that A7: x1 in F . k by XBOOLE_0:def_1; take y = f . x1; ::_thesis: ex y being Element of ExtREAL st S1[k,y] for x being set st x in F . k holds y = f . x proof let x be set ; ::_thesis: ( x in F . k implies y = f . x ) A8: rng F c= bool X by XBOOLE_1:1; then reconsider x1 = x1 as Element of X by A5, A7; assume A9: x in F . k ; ::_thesis: y = f . x then reconsider x = x as Element of X by A5, A8; f . x = f . x1 by A2, A4, A7, A9; hence y = f . x ; ::_thesis: verum end; hence ex y being Element of ExtREAL st S1[k,y] ; ::_thesis: verum end; end; end; hence ex y being Element of ExtREAL st S1[k,y] ; ::_thesis: verum end; consider a being FinSequence of ExtREAL such that A10: ( dom a = Seg (len F) & ( for k being Nat st k in Seg (len F) holds S1[k,a . k] ) ) from FINSEQ_1:sch_5(A3); take F ; ::_thesis: ex a being FinSequence of ExtREAL st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & ( for x being set st x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) ) take a ; ::_thesis: ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & ( for x being set st x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) ) A11: for x being set st x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) proof let x be set ; ::_thesis: ( x in dom f implies ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) assume x in dom f ; ::_thesis: ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) deffunc H1( Nat) -> Element of ExtREAL = (a . \$1) * ((chi ((F . \$1),X)) . x); consider ax being FinSequence of ExtREAL such that A12: ( len ax = len F & ( for k being Nat st k in dom ax holds ax . k = H1(k) ) ) from FINSEQ_2:sch_1(); take ax ; ::_thesis: ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) thus ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) by A10, A12, FINSEQ_1:def_3; ::_thesis: verum end; for n being Nat st n in dom F holds for x being set st x in F . n holds a . n = f . x proof let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds a . n = f . x ) assume n in dom F ; ::_thesis: for x being set st x in F . n holds a . n = f . x then n in Seg (len F) by FINSEQ_1:def_3; hence for x being set st x in F . n holds a . n = f . x by A10; ::_thesis: verum end; hence ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) & ( for x being set st x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) ) by A1, A10, A11, FINSEQ_1:def_3; ::_thesis: verum end; theorem Th4: :: MESFUNC3:4 for X being set for F being FinSequence of X holds ( F is disjoint_valued iff for i, j being Nat st i in dom F & j in dom F & i <> j holds F . i misses F . j ) proof let X be set ; ::_thesis: for F being FinSequence of X holds ( F is disjoint_valued iff for i, j being Nat st i in dom F & j in dom F & i <> j holds F . i misses F . j ) let F be FinSequence of X; ::_thesis: ( F is disjoint_valued iff for i, j being Nat st i in dom F & j in dom F & i <> j holds F . i misses F . j ) now__::_thesis:_(_(_for_i,_j_being_Nat_st_i_in_dom_F_&_j_in_dom_F_&_i_<>_j_holds_ F_._i_misses_F_._j_)_implies_F_is_disjoint_valued_) assume A1: for i, j being Nat st i in dom F & j in dom F & i <> j holds F . i misses F . j ; ::_thesis: F is disjoint_valued for x, y being set st x <> y holds F . x misses F . y proof let x, y be set ; ::_thesis: ( x <> y implies F . x misses F . y ) assume A2: x <> y ; ::_thesis: F . x misses F . y percases ( ( x in dom F & y in dom F ) or not x in dom F or not y in dom F ) ; suppose ( x in dom F & y in dom F ) ; ::_thesis: F . x misses F . y hence F . x misses F . y by A1, A2; ::_thesis: verum end; suppose not x in dom F ; ::_thesis: F . x misses F . y then F . x = {} by FUNCT_1:def_2; hence F . x misses F . y by XBOOLE_1:65; ::_thesis: verum end; suppose not y in dom F ; ::_thesis: F . x misses F . y then F . y = {} by FUNCT_1:def_2; hence F . x misses F . y by XBOOLE_1:65; ::_thesis: verum end; end; end; hence F is disjoint_valued by PROB_2:def_2; ::_thesis: verum end; hence ( F is disjoint_valued iff for i, j being Nat st i in dom F & j in dom F & i <> j holds F . i misses F . j ) by PROB_2:def_2; ::_thesis: verum end; theorem Th5: :: MESFUNC3:5 for X being non empty set for A being set for S being SigmaField of X for F being Finite_Sep_Sequence of S for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds G . i = A /\ (F . i) ) holds G is Finite_Sep_Sequence of S proof let X be non empty set ; ::_thesis: for A being set for S being SigmaField of X for F being Finite_Sep_Sequence of S for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds G . i = A /\ (F . i) ) holds G is Finite_Sep_Sequence of S let A be set ; ::_thesis: for S being SigmaField of X for F being Finite_Sep_Sequence of S for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds G . i = A /\ (F . i) ) holds G is Finite_Sep_Sequence of S let S be SigmaField of X; ::_thesis: for F being Finite_Sep_Sequence of S for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds G . i = A /\ (F . i) ) holds G is Finite_Sep_Sequence of S let F be Finite_Sep_Sequence of S; ::_thesis: for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds G . i = A /\ (F . i) ) holds G is Finite_Sep_Sequence of S let G be FinSequence of S; ::_thesis: ( dom G = dom F & ( for i being Nat st i in dom G holds G . i = A /\ (F . i) ) implies G is Finite_Sep_Sequence of S ) assume that A1: dom G = dom F and A2: for i being Nat st i in dom G holds G . i = A /\ (F . i) ; ::_thesis: G is Finite_Sep_Sequence of S now__::_thesis:_for_i,_j_being_Nat_st_i_in_dom_G_&_j_in_dom_G_&_i_<>_j_holds_ G_._i_misses_G_._j let i, j be Nat; ::_thesis: ( i in dom G & j in dom G & i <> j implies G . i misses G . j ) assume that A3: i in dom G and A4: j in dom G and A5: i <> j ; ::_thesis: G . i misses G . j A6: F . i misses F . j by A1, A3, A4, A5, Th4; (A /\ (F . i)) /\ (A /\ (F . j)) = A /\ ((F . i) /\ (A /\ (F . j))) by XBOOLE_1:16 .= A /\ (((F . i) /\ (F . j)) /\ A) by XBOOLE_1:16 .= A /\ ({} /\ A) by A6, XBOOLE_0:def_7 .= {} ; then A /\ (F . i) misses A /\ (F . j) by XBOOLE_0:def_7; then G . i misses A /\ (F . j) by A2, A3; hence G . i misses G . j by A2, A4; ::_thesis: verum end; hence G is Finite_Sep_Sequence of S by Th4; ::_thesis: verum end; theorem Th6: :: MESFUNC3:6 for X being non empty set for A being set for F, G being FinSequence of X st dom G = dom F & ( for i being Nat st i in dom G holds G . i = A /\ (F . i) ) holds union (rng G) = A /\ (union (rng F)) proof let X be non empty set ; ::_thesis: for A being set for F, G being FinSequence of X st dom G = dom F & ( for i being Nat st i in dom G holds G . i = A /\ (F . i) ) holds union (rng G) = A /\ (union (rng F)) let A be set ; ::_thesis: for F, G being FinSequence of X st dom G = dom F & ( for i being Nat st i in dom G holds G . i = A /\ (F . i) ) holds union (rng G) = A /\ (union (rng F)) let F, G be FinSequence of X; ::_thesis: ( dom G = dom F & ( for i being Nat st i in dom G holds G . i = A /\ (F . i) ) implies union (rng G) = A /\ (union (rng F)) ) assume that A1: dom G = dom F and A2: for i being Nat st i in dom G holds G . i = A /\ (F . i) ; ::_thesis: union (rng G) = A /\ (union (rng F)) thus union (rng G) c= A /\ (union (rng F)) :: according to XBOOLE_0:def_10 ::_thesis: A /\ (union (rng F)) c= union (rng G) proof let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in union (rng G) or r in A /\ (union (rng F)) ) assume r in union (rng G) ; ::_thesis: r in A /\ (union (rng F)) then consider E being set such that A3: r in E and A4: E in rng G by TARSKI:def_4; consider s being set such that A5: s in dom G and A6: E = G . s by A4, FUNCT_1:def_3; reconsider s = s as Element of NAT by A5; A7: r in A /\ (F . s) by A2, A3, A5, A6; then A8: r in F . s by XBOOLE_0:def_4; F . s in rng F by A1, A5, FUNCT_1:3; then A9: r in union (rng F) by A8, TARSKI:def_4; r in A by A7, XBOOLE_0:def_4; hence r in A /\ (union (rng F)) by A9, XBOOLE_0:def_4; ::_thesis: verum end; let r be set ; :: according to TARSKI:def_3 ::_thesis: ( not r in A /\ (union (rng F)) or r in union (rng G) ) assume A10: r in A /\ (union (rng F)) ; ::_thesis: r in union (rng G) then A11: r in A by XBOOLE_0:def_4; r in union (rng F) by A10, XBOOLE_0:def_4; then consider E being set such that A12: r in E and A13: E in rng F by TARSKI:def_4; consider s being set such that A14: s in dom F and A15: E = F . s by A13, FUNCT_1:def_3; reconsider s = s as Element of NAT by A14; A /\ E = G . s by A1, A2, A14, A15; then A16: r in G . s by A11, A12, XBOOLE_0:def_4; G . s in rng G by A1, A14, FUNCT_1:3; hence r in union (rng G) by A16, TARSKI:def_4; ::_thesis: verum end; theorem Th7: :: MESFUNC3:7 for X being set for F being FinSequence of X for i being Nat st i in dom F holds ( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i ) proof let X be set ; ::_thesis: for F being FinSequence of X for i being Nat st i in dom F holds ( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i ) let F be FinSequence of X; ::_thesis: for i being Nat st i in dom F holds ( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i ) let i be Nat; ::_thesis: ( i in dom F implies ( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i ) ) assume A1: i in dom F ; ::_thesis: ( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i ) hence F . i c= union (rng F) by FUNCT_1:3, ZFMISC_1:74; ::_thesis: (F . i) /\ (union (rng F)) = F . i F . i in rng F by A1, FUNCT_1:3; hence (F . i) /\ (union (rng F)) = F . i by XBOOLE_1:28, ZFMISC_1:74; ::_thesis: verum end; theorem Th8: :: MESFUNC3:8 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for F being Finite_Sep_Sequence of S holds dom F = dom (M * F) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for F being Finite_Sep_Sequence of S holds dom F = dom (M * F) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for F being Finite_Sep_Sequence of S holds dom F = dom (M * F) let M be sigma_Measure of S; ::_thesis: for F being Finite_Sep_Sequence of S holds dom F = dom (M * F) let F be Finite_Sep_Sequence of S; ::_thesis: dom F = dom (M * F) dom M = S by FUNCT_2:def_1; then rng F c= dom M ; hence dom F = dom (M * F) by RELAT_1:27; ::_thesis: verum end; theorem Th9: :: MESFUNC3:9 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for F being Finite_Sep_Sequence of S holds M . (union (rng F)) = Sum (M * F) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for F being Finite_Sep_Sequence of S holds M . (union (rng F)) = Sum (M * F) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for F being Finite_Sep_Sequence of S holds M . (union (rng F)) = Sum (M * F) let M be sigma_Measure of S; ::_thesis: for F being Finite_Sep_Sequence of S holds M . (union (rng F)) = Sum (M * F) let F be Finite_Sep_Sequence of S; ::_thesis: M . (union (rng F)) = Sum (M * F) reconsider F1 = M * F as FinSequence of ExtREAL ; consider f being Function of NAT,ExtREAL such that A1: Sum F1 = f . (len F1) and A2: f . 0 = 0. and A3: for i being Element of NAT st i < len F1 holds f . (i + 1) = (f . i) + (F1 . (i + 1)) by EXTREAL1:def_2; consider G being Sep_Sequence of S such that A4: union (rng F) = union (rng G) and A5: for n being Nat st n in dom F holds F . n = G . n and A6: for m being Nat st not m in dom F holds G . m = {} by MESFUNC2:30; defpred S1[ Nat] means ( \$1 <= len F1 implies (Ser (M * G)) . \$1 = f . \$1 ); reconsider G1 = M * G as Num of rng (M * G) by SUPINF_2:def_10; A7: dom G = NAT by FUNCT_2:def_1; A8: Ser (M * G) = Ser ((rng (M * G)),G1) by SUPINF_2:def_15; A9: for i being Nat st i < len F1 holds (Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (F1 . (i + 1)) proof let i be Nat; ::_thesis: ( i < len F1 implies (Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (F1 . (i + 1)) ) assume i < len F1 ; ::_thesis: (Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (F1 . (i + 1)) then ( 1 <= i + 1 & i + 1 <= len F1 ) by NAT_1:11, NAT_1:13; then i + 1 in dom F1 by FINSEQ_3:25; then A10: i + 1 in dom F by Th8; reconsider i = i as Element of NAT by ORDINAL1:def_12; (Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (G1 . (i + 1)) by A8, SUPINF_2:def_11 .= ((Ser (M * G)) . i) + (M . (G . (i + 1))) by A7, FUNCT_1:13 .= ((Ser (M * G)) . i) + (M . (F . (i + 1))) by A5, A10 ; hence (Ser (M * G)) . (i + 1) = ((Ser (M * G)) . i) + (F1 . (i + 1)) by A10, FUNCT_1:13; ::_thesis: verum end; A11: for k being Nat st S1[k] holds S1[k + 1] proof A12: for i being Nat st i < len F1 holds f . (i + 1) = (f . i) + (F1 . (i + 1)) proof let i be Nat; ::_thesis: ( i < len F1 implies f . (i + 1) = (f . i) + (F1 . (i + 1)) ) i in NAT by ORDINAL1:def_12; hence ( i < len F1 implies f . (i + 1) = (f . i) + (F1 . (i + 1)) ) by A3; ::_thesis: verum end; let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A13: S1[k] ; ::_thesis: S1[k + 1] assume k + 1 <= len F1 ; ::_thesis: (Ser (M * G)) . (k + 1) = f . (k + 1) then A14: k < len F1 by NAT_1:13; then (Ser (M * G)) . (k + 1) = (f . k) + (F1 . (k + 1)) by A9, A13; hence (Ser (M * G)) . (k + 1) = f . (k + 1) by A12, A14; ::_thesis: verum end; defpred S2[ Nat] means ( \$1 >= len F1 implies (Ser (M * G)) . \$1 = (Ser (M * G)) . (len F1) ); A15: for k being Nat st S2[k] holds S2[k + 1] proof let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A16: S2[k] ; ::_thesis: S2[k + 1] assume A17: k + 1 >= len F1 ; ::_thesis: (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) reconsider k = k as Element of NAT by ORDINAL1:def_12; now__::_thesis:_(_(_k_>=_len_F1_&_(Ser_(M_*_G))_._(k_+_1)_=_(Ser_(M_*_G))_._(len_F1)_)_or_(_k_<_len_F1_&_(Ser_(M_*_G))_._(k_+_1)_=_(Ser_(M_*_G))_._(len_F1)_)_) percases ( k >= len F1 or k < len F1 ) ; caseA18: k >= len F1 ; ::_thesis: (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) then k + 1 > len F1 by NAT_1:13; then not k + 1 in Seg (len F1) by FINSEQ_1:1; then not k + 1 in dom F1 by FINSEQ_1:def_3; then A19: not k + 1 in dom F by Th8; A20: G1 . (k + 1) = M . (G . (k + 1)) by A7, FUNCT_1:13 .= M . {} by A6, A19 .= 0. by VALUED_0:def_19 ; (Ser (M * G)) . (k + 1) = ((Ser (M * G)) . (len F1)) + (G1 . (k + 1)) by A8, A16, A18, SUPINF_2:def_11; hence (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) by A20, XXREAL_3:4; ::_thesis: verum end; case k < len F1 ; ::_thesis: (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) then k + 1 <= len F1 by NAT_1:13; hence (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) by A17, XXREAL_0:1; ::_thesis: verum end; end; end; hence (Ser (M * G)) . (k + 1) = (Ser (M * G)) . (len F1) ; ::_thesis: verum end; defpred S3[ Nat] means ( \$1 < len F1 implies (Ser (M * G)) . ((len F1) - \$1) <= (Ser (M * G)) . (len F1) ); A21: M * G is V103() by MEASURE2:1; A22: for k being Nat st S3[k] holds S3[k + 1] proof let k be Nat; ::_thesis: ( S3[k] implies S3[k + 1] ) assume A23: S3[k] ; ::_thesis: S3[k + 1] assume A24: k + 1 < len F1 ; ::_thesis: (Ser (M * G)) . ((len F1) - (k + 1)) <= (Ser (M * G)) . (len F1) then consider k9 being Nat such that A25: len F1 = (k + 1) + k9 by NAT_1:10; reconsider k9 = k9 as Element of NAT by ORDINAL1:def_12; ( k <= k + 1 & (Ser (M * G)) . k9 <= (Ser (M * G)) . (k9 + 1) ) by A21, NAT_1:11, SUPINF_2:40; hence (Ser (M * G)) . ((len F1) - (k + 1)) <= (Ser (M * G)) . (len F1) by A23, A24, A25, XXREAL_0:2; ::_thesis: verum end; not 0 in Seg (len F) by FINSEQ_1:1; then not 0 in dom F by FINSEQ_1:def_3; then A26: G . 0 = {} by A6; (Ser (M * G)) . 0 = G1 . 0 by A8, SUPINF_2:def_11; then A27: (Ser (M * G)) . 0 = M . (G . 0) by A7, FUNCT_1:13 .= 0. by A26, VALUED_0:def_19 ; then A28: S1[ 0 ] by A2; A29: for k being Nat holds S1[k] from NAT_1:sch_2(A28, A11); A30: S3[ 0 ] ; A31: for i being Nat holds S3[i] from NAT_1:sch_2(A30, A22); A32: for i being Nat st i < len F1 holds (Ser (M * G)) . i <= (Ser (M * G)) . (len F1) proof let i be Nat; ::_thesis: ( i < len F1 implies (Ser (M * G)) . i <= (Ser (M * G)) . (len F1) ) A33: len F1 <= (len F1) + i by NAT_1:11; assume i < len F1 ; ::_thesis: (Ser (M * G)) . i <= (Ser (M * G)) . (len F1) then consider k being Nat such that A34: len F1 = i + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; k = (len F1) - i by A34; then A35: k <= len F1 by A33, XREAL_1:20; (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1) proof now__::_thesis:_(_(_k_=_len_F1_&_(Ser_(M_*_G))_._((len_F1)_-_k)_<=_(Ser_(M_*_G))_._(len_F1)_)_or_(_k_<_len_F1_&_(Ser_(M_*_G))_._((len_F1)_-_k)_<=_(Ser_(M_*_G))_._(len_F1)_)_) percases ( k = len F1 or k < len F1 ) by A35, XXREAL_0:1; case k = len F1 ; ::_thesis: (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1) hence (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1) by A27, A21, SUPINF_2:40; ::_thesis: verum end; case k < len F1 ; ::_thesis: (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1) hence (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1) by A31; ::_thesis: verum end; end; end; hence (Ser (M * G)) . ((len F1) - k) <= (Ser (M * G)) . (len F1) ; ::_thesis: verum end; hence (Ser (M * G)) . i <= (Ser (M * G)) . (len F1) by A34; ::_thesis: verum end; A36: S2[ 0 ] ; A37: for k being Nat holds S2[k] from NAT_1:sch_2(A36, A15); for z being ext-real number st z in rng (Ser (M * G)) holds z <= (Ser (M * G)) . (len F1) proof let z be ext-real number ; ::_thesis: ( z in rng (Ser (M * G)) implies z <= (Ser (M * G)) . (len F1) ) assume z in rng (Ser (M * G)) ; ::_thesis: z <= (Ser (M * G)) . (len F1) then consider n being set such that A38: n in dom (Ser (M * G)) and A39: z = (Ser (M * G)) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A38; now__::_thesis:_(_(_n_<_len_F1_&_z_<=_(Ser_(M_*_G))_._(len_F1)_)_or_(_n_>=_len_F1_&_z_<=_(Ser_(M_*_G))_._(len_F1)_)_) percases ( n < len F1 or n >= len F1 ) ; case n < len F1 ; ::_thesis: z <= (Ser (M * G)) . (len F1) hence z <= (Ser (M * G)) . (len F1) by A32, A39; ::_thesis: verum end; case n >= len F1 ; ::_thesis: z <= (Ser (M * G)) . (len F1) hence z <= (Ser (M * G)) . (len F1) by A37, A39; ::_thesis: verum end; end; end; hence z <= (Ser (M * G)) . (len F1) ; ::_thesis: verum end; then A40: (Ser (M * G)) . (len F1) is UpperBound of rng (Ser (M * G)) by XXREAL_2:def_1; dom (Ser (M * G)) = NAT by FUNCT_2:def_1; then A41: (Ser (M * G)) . (len F1) = sup (rng (Ser (M * G))) by A40, FUNCT_1:3, XXREAL_2:55; M . (union (rng F)) = SUM (M * G) by A4, MEASURE1:def_6 .= sup (rng (Ser (M * G))) ; hence M . (union (rng F)) = Sum (M * F) by A1, A29, A41; ::_thesis: verum end; theorem Th10: :: MESFUNC3:10 for F, G being FinSequence of ExtREAL for a being R_eal st ( a is real or for i being Nat st i in dom F holds F . i < 0. or for i being Nat st i in dom F holds 0. < F . i ) & dom F = dom G & ( for i being Nat st i in dom G holds G . i = a * (F . i) ) holds Sum G = a * (Sum F) proof let F, G be FinSequence of ExtREAL ; ::_thesis: for a being R_eal st ( a is real or for i being Nat st i in dom F holds F . i < 0. or for i being Nat st i in dom F holds 0. < F . i ) & dom F = dom G & ( for i being Nat st i in dom G holds G . i = a * (F . i) ) holds Sum G = a * (Sum F) let a be R_eal; ::_thesis: ( ( a is real or for i being Nat st i in dom F holds F . i < 0. or for i being Nat st i in dom F holds 0. < F . i ) & dom F = dom G & ( for i being Nat st i in dom G holds G . i = a * (F . i) ) implies Sum G = a * (Sum F) ) assume that A1: ( a is real or for i being Nat st i in dom F holds F . i < 0. or for i being Nat st i in dom F holds 0. < F . i ) and A2: dom F = dom G and A3: for i being Nat st i in dom G holds G . i = a * (F . i) ; ::_thesis: Sum G = a * (Sum F) consider g being Function of NAT,ExtREAL such that A4: Sum G = g . (len G) and A5: g . 0 = 0. and A6: for i being Element of NAT st i < len G holds g . (i + 1) = (g . i) + (G . (i + 1)) by EXTREAL1:def_2; consider f being Function of NAT,ExtREAL such that A7: Sum F = f . (len F) and A8: f . 0 = 0. and A9: for i being Element of NAT st i < len F holds f . (i + 1) = (f . i) + (F . (i + 1)) by EXTREAL1:def_2; defpred S1[ Nat] means ( \$1 <= len G implies g . \$1 = a * (f . \$1) ); A10: for i being Nat st S1[i] holds S1[i + 1] proof let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A11: S1[i] ; ::_thesis: S1[i + 1] assume A12: i + 1 <= len G ; ::_thesis: g . (i + 1) = a * (f . (i + 1)) reconsider i = i as Element of NAT by ORDINAL1:def_12; 1 <= i + 1 by NAT_1:11; then A13: i + 1 in dom G by A12, FINSEQ_3:25; then i + 1 in Seg (len F) by A2, FINSEQ_1:def_3; then i + 1 <= len F by FINSEQ_1:1; then A14: i < len F by NAT_1:13; i < len G by A12, NAT_1:13; then A15: g . (i + 1) = (g . i) + (G . (i + 1)) by A6 .= (a * (f . i)) + (a * (F . (i + 1))) by A3, A11, A12, A13, NAT_1:13 ; now__::_thesis:_(_(_a_is_real_&_g_._(i_+_1)_=_a_*_(f_._(i_+_1))_)_or_(_(_for_i_being_Nat_st_i_in_dom_F_holds_ F_._i_<_0._)_&_g_._(i_+_1)_=_a_*_(f_._(i_+_1))_)_or_(_(_for_i_being_Nat_st_i_in_dom_F_holds_ 0._<_F_._i_)_&_g_._(i_+_1)_=_a_*_(f_._(i_+_1))_)_) percases ( a is real or for i being Nat st i in dom F holds F . i < 0. or for i being Nat st i in dom F holds 0. < F . i ) by A1; case a is real ; ::_thesis: g . (i + 1) = a * (f . (i + 1)) then g . (i + 1) = a * ((f . i) + (F . (i + 1))) by A15, XXREAL_3:95; hence g . (i + 1) = a * (f . (i + 1)) by A9, A14; ::_thesis: verum end; caseA16: for i being Nat st i in dom F holds F . i < 0. ; ::_thesis: g . (i + 1) = a * (f . (i + 1)) defpred S2[ Nat] means ( \$1 < len F implies f . \$1 <= 0. ); A17: for i being Nat st S2[i] holds S2[i + 1] proof let i be Nat; ::_thesis: ( S2[i] implies S2[i + 1] ) assume A18: S2[i] ; ::_thesis: S2[i + 1] assume A19: i + 1 < len F ; ::_thesis: f . (i + 1) <= 0. reconsider i = i as Element of NAT by ORDINAL1:def_12; 1 <= i + 1 by NAT_1:12; then i + 1 in dom F by A19, FINSEQ_3:25; then A20: F . (i + 1) < 0. by A16; i < len F by A19, NAT_1:13; then f . (i + 1) = (f . i) + (F . (i + 1)) by A9; hence f . (i + 1) <= 0. by A18, A19, A20, NAT_1:13; ::_thesis: verum end; A21: S2[ 0 ] by A8; for i being Nat holds S2[i] from NAT_1:sch_2(A21, A17); then A22: ( f . i < 0. or f . i = 0. ) by A14; F . (i + 1) < 0. by A2, A13, A16; then g . (i + 1) = a * ((f . i) + (F . (i + 1))) by A15, A22, XXREAL_3:97; hence g . (i + 1) = a * (f . (i + 1)) by A9, A14; ::_thesis: verum end; caseA23: for i being Nat st i in dom F holds 0. < F . i ; ::_thesis: g . (i + 1) = a * (f . (i + 1)) defpred S2[ Nat] means ( \$1 < len F implies 0. <= f . \$1 ); A24: for i being Nat st S2[i] holds S2[i + 1] proof let i be Nat; ::_thesis: ( S2[i] implies S2[i + 1] ) assume A25: S2[i] ; ::_thesis: S2[i + 1] assume A26: i + 1 < len F ; ::_thesis: 0. <= f . (i + 1) reconsider i = i as Element of NAT by ORDINAL1:def_12; 1 <= i + 1 by NAT_1:12; then i + 1 in dom F by A26, FINSEQ_3:25; then A27: 0. < F . (i + 1) by A23; i < len F by A26, NAT_1:13; then f . (i + 1) = (f . i) + (F . (i + 1)) by A9; hence 0. <= f . (i + 1) by A25, A26, A27, NAT_1:13; ::_thesis: verum end; A28: S2[ 0 ] by A8; for i being Nat holds S2[i] from NAT_1:sch_2(A28, A24); then A29: ( 0. < f . i or f . i = 0. ) by A14; 0. < F . (i + 1) by A2, A13, A23; then g . (i + 1) = a * ((f . i) + (F . (i + 1))) by A15, A29, XXREAL_3:96; hence g . (i + 1) = a * (f . (i + 1)) by A9, A14; ::_thesis: verum end; end; end; hence g . (i + 1) = a * (f . (i + 1)) ; ::_thesis: verum end; A30: S1[ 0 ] by A8, A5; A31: for i being Nat holds S1[i] from NAT_1:sch_2(A30, A10); Seg (len F) = dom G by A2, FINSEQ_1:def_3 .= Seg (len G) by FINSEQ_1:def_3 ; then a * (Sum F) = a * (f . (len G)) by A7, FINSEQ_1:6 .= g . (len G) by A31 ; hence Sum G = a * (Sum F) by A4; ::_thesis: verum end; theorem Th11: :: MESFUNC3:11 for F being FinSequence of REAL holds F is FinSequence of ExtREAL proof let F be FinSequence of REAL ; ::_thesis: F is FinSequence of ExtREAL rng F c= ExtREAL by NUMBERS:31, XBOOLE_1:1; hence F is FinSequence of ExtREAL by FINSEQ_1:def_4; ::_thesis: verum end; definition let X be non empty set ; let S be SigmaField of X; let f be PartFunc of X,ExtREAL; let F be Finite_Sep_Sequence of S; let a be FinSequence of ExtREAL ; predF,a are_Re-presentation_of f means :Def1: :: MESFUNC3:def 1 ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ); end; :: deftheorem Def1 defines are_Re-presentation_of MESFUNC3:def_1_:_ for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for F being Finite_Sep_Sequence of S for a being FinSequence of ExtREAL holds ( F,a are_Re-presentation_of f iff ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) ); theorem :: MESFUNC3:12 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f let f be PartFunc of X,ExtREAL; ::_thesis: ( f is_simple_func_in S implies ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f ) assume f is_simple_func_in S ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f then consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that A1: ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) and for x being set st x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) by Th3; take F ; ::_thesis: ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f take a ; ::_thesis: F,a are_Re-presentation_of f thus F,a are_Re-presentation_of f by A1, Def1; ::_thesis: verum end; theorem Th13: :: MESFUNC3:13 for X being non empty set for S being SigmaField of X for F being Finite_Sep_Sequence of S ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds ( G . n <> {} & ex m being Nat st ( m in dom F & F . m = G . n ) ) ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for F being Finite_Sep_Sequence of S ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds ( G . n <> {} & ex m being Nat st ( m in dom F & F . m = G . n ) ) ) ) let S be SigmaField of X; ::_thesis: for F being Finite_Sep_Sequence of S ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds ( G . n <> {} & ex m being Nat st ( m in dom F & F . m = G . n ) ) ) ) let F be Finite_Sep_Sequence of S; ::_thesis: ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds ( G . n <> {} & ex m being Nat st ( m in dom F & F . m = G . n ) ) ) ) defpred S1[ Nat] means for F being Finite_Sep_Sequence of S st len F = \$1 holds ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds ( G . n <> {} & ex m being Nat st ( m in dom F & F . m = G . n ) ) ) ); A1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] let F be Finite_Sep_Sequence of S; ::_thesis: ( len F = n + 1 implies ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds ( G . n <> {} & ex m being Nat st ( m in dom F & F . m = G . n ) ) ) ) ) assume A3: len F = n + 1 ; ::_thesis: ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds ( G . n <> {} & ex m being Nat st ( m in dom F & F . m = G . n ) ) ) ) reconsider n = n as Element of NAT by ORDINAL1:def_12; reconsider F1 = F | (Seg n) as Finite_Sep_Sequence of S by MESFUNC2:33; A4: n <= len F by A3, NAT_1:11; then A5: len F1 = n by FINSEQ_1:17; then consider G1 being Finite_Sep_Sequence of S such that A6: union (rng F1) = union (rng G1) and A7: for n being Nat st n in dom G1 holds ( G1 . n <> {} & ex m being Nat st ( m in dom F1 & F1 . m = G1 . n ) ) by A2; A8: ( dom F = dom (F1 ^ <*(F . (n + 1))*>) & ( for k being Nat st k in dom F holds F . k = (F1 ^ <*(F . (n + 1))*>) . k ) ) proof thus dom (F1 ^ <*(F . (n + 1))*>) = Seg ((len F1) + (len <*(F . (n + 1))*>)) by FINSEQ_1:def_7 .= Seg (n + 1) by A5, FINSEQ_1:39 .= dom F by A3, FINSEQ_1:def_3 ; ::_thesis: for k being Nat st k in dom F holds F . k = (F1 ^ <*(F . (n + 1))*>) . k let k be Nat; ::_thesis: ( k in dom F implies F . k = (F1 ^ <*(F . (n + 1))*>) . k ) assume A9: k in dom F ; ::_thesis: F . k = (F1 ^ <*(F . (n + 1))*>) . k now__::_thesis:_(_(_k_in_dom_F1_&_F_._k_=_(F1_^_<*(F_._(n_+_1))*>)_._k_)_or_(_not_k_in_dom_F1_&_F_._k_=_(F1_^_<*(F_._(n_+_1))*>)_._k_)_) percases ( k in dom F1 or not k in dom F1 ) ; caseA10: k in dom F1 ; ::_thesis: F . k = (F1 ^ <*(F . (n + 1))*>) . k then k in Seg n by A4, FINSEQ_1:17; then k <= n by FINSEQ_1:1; then A11: (F | n) . k = F . k by FINSEQ_3:112; (F1 ^ <*(F . (n + 1))*>) . k = F1 . k by A10, FINSEQ_1:def_7; hence F . k = (F1 ^ <*(F . (n + 1))*>) . k by A11, FINSEQ_1:def_15; ::_thesis: verum end; caseA12: not k in dom F1 ; ::_thesis: F . k = (F1 ^ <*(F . (n + 1))*>) . k A13: k in Seg (n + 1) by A3, A9, FINSEQ_1:def_3; not k in Seg n by A4, A12, FINSEQ_1:17; then ( not 1 <= k or not k <= n ) by FINSEQ_1:1; then A14: not k < n + 1 by A13, FINSEQ_1:1, NAT_1:13; dom <*(F . (n + 1))*> = Seg 1 by FINSEQ_1:def_8; then A15: 1 in dom <*(F . (n + 1))*> by FINSEQ_1:2, TARSKI:def_1; A16: k <= n + 1 by A13, FINSEQ_1:1; then (F1 ^ <*(F . (n + 1))*>) . k = (F1 ^ <*(F . (n + 1))*>) . ((len F1) + 1) by A5, A14, XXREAL_0:1 .= <*(F . (n + 1))*> . 1 by A15, FINSEQ_1:def_7 .= F . (n + 1) by FINSEQ_1:def_8 ; hence F . k = (F1 ^ <*(F . (n + 1))*>) . k by A14, A16, XXREAL_0:1; ::_thesis: verum end; end; end; hence F . k = (F1 ^ <*(F . (n + 1))*>) . k ; ::_thesis: verum end; then A17: F = F1 ^ <*(F . (n + 1))*> by FINSEQ_1:13; ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) ) ) proof now__::_thesis:_(_(_F_._(n_+_1)_=_{}_&_ex_G,_G_being_Finite_Sep_Sequence_of_S_st_ (_union_(rng_F)_=_union_(rng_G)_&_(_for_k_being_Nat_st_k_in_dom_G_holds_ (_G_._k_<>_{}_&_ex_m_being_Nat_st_ (_m_in_dom_F_&_F_._m_=_G_._k_)_)_)_)_)_or_(_F_._(n_+_1)_<>_{}_&_ex_G,_G_being_Finite_Sep_Sequence_of_S_st_ (_union_(rng_F)_=_union_(rng_G)_&_(_for_k_being_Nat_st_k_in_dom_G_holds_ (_G_._k_<>_{}_&_ex_m_being_Nat_st_ (_m_in_dom_F_&_F_._m_=_G_._k_)_)_)_)_)_) percases ( F . (n + 1) = {} or F . (n + 1) <> {} ) ; case F . (n + 1) = {} ; ::_thesis: ex G, G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) ) ) then A18: rng <*(F . (n + 1))*> = {{}} by FINSEQ_1:38; take G = G1; ::_thesis: ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) ) ) A19: for k being Nat st k in dom G holds ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) proof let k be Nat; ::_thesis: ( k in dom G implies ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) ) A20: dom F1 c= dom F by A8, FINSEQ_1:26; assume A21: k in dom G ; ::_thesis: ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) then consider m being Nat such that A22: m in dom F1 and A23: F1 . m = G . k by A7; F1 . m = F . m by A17, A22, FINSEQ_1:def_7; hence ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) by A7, A21, A22, A23, A20; ::_thesis: verum end; rng F = (rng F1) \/ (rng <*(F . (n + 1))*>) by A17, FINSEQ_1:31; then union (rng F) = (union (rng F1)) \/ (union (rng <*(F . (n + 1))*>)) by ZFMISC_1:78 .= (union (rng F1)) \/ {} by A18, ZFMISC_1:25 .= union (rng G) by A6 ; hence ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) ) ) by A19; ::_thesis: verum end; caseA24: F . (n + 1) <> {} ; ::_thesis: ex G, G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) ) ) A25: for k, m being set st k <> m holds (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m proof let k, m be set ; ::_thesis: ( k <> m implies (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m ) assume A26: k <> m ; ::_thesis: (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m now__::_thesis:_(_(_k_in_dom_(G1_^_<*(F_._(n_+_1))*>)_&_m_in_dom_(G1_^_<*(F_._(n_+_1))*>)_&_(G1_^_<*(F_._(n_+_1))*>)_._k_misses_(G1_^_<*(F_._(n_+_1))*>)_._m_)_or_(_(_not_k_in_dom_(G1_^_<*(F_._(n_+_1))*>)_or_not_m_in_dom_(G1_^_<*(F_._(n_+_1))*>)_)_&_(G1_^_<*(F_._(n_+_1))*>)_._k_misses_(G1_^_<*(F_._(n_+_1))*>)_._m_)_) percases ( ( k in dom (G1 ^ <*(F . (n + 1))*>) & m in dom (G1 ^ <*(F . (n + 1))*>) ) or not k in dom (G1 ^ <*(F . (n + 1))*>) or not m in dom (G1 ^ <*(F . (n + 1))*>) ) ; caseA27: ( k in dom (G1 ^ <*(F . (n + 1))*>) & m in dom (G1 ^ <*(F . (n + 1))*>) ) ; ::_thesis: (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m then reconsider k = k, m = m as Element of NAT ; now__::_thesis:_(_(_k_=_len_(G1_^_<*(F_._(n_+_1))*>)_&_(G1_^_<*(F_._(n_+_1))*>)_._k_misses_(G1_^_<*(F_._(n_+_1))*>)_._m_)_or_(_k_<>_len_(G1_^_<*(F_._(n_+_1))*>)_&_(G1_^_<*(F_._(n_+_1))*>)_._k_misses_(G1_^_<*(F_._(n_+_1))*>)_._m_)_) percases ( k = len (G1 ^ <*(F . (n + 1))*>) or k <> len (G1 ^ <*(F . (n + 1))*>) ) ; case k = len (G1 ^ <*(F . (n + 1))*>) ; ::_thesis: (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m then k = (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22; then A28: k = (len G1) + 1 by FINSEQ_1:39; 1 <= len <*(F . (n + 1))*> by FINSEQ_1:39; then A29: (G1 ^ <*(F . (n + 1))*>) . k = <*(F . (n + 1))*> . 1 by A28, FINSEQ_1:65 .= F . (n + 1) by FINSEQ_1:def_8 ; A30: m in Seg (len (G1 ^ <*(F . (n + 1))*>)) by A27, FINSEQ_1:def_3; then m in Seg ((len G1) + (len <*(F . (n + 1))*>)) by FINSEQ_1:22; then m in Seg ((len G1) + 1) by FINSEQ_1:39; then m <= (len G1) + 1 by FINSEQ_1:1; then m < (len G1) + 1 by A26, A28, XXREAL_0:1; then A31: m <= len G1 by NAT_1:13; 1 <= m by A30, FINSEQ_1:1; then A32: m in dom G1 by A31, FINSEQ_3:25; then consider m1 being Nat such that A33: m1 in dom F1 and A34: F1 . m1 = G1 . m by A7; m1 in Seg (len F1) by A33, FINSEQ_1:def_3; then m1 <= n by A5, FINSEQ_1:1; then A35: m1 <> n + 1 by NAT_1:13; (G1 ^ <*(F . (n + 1))*>) . m = G1 . m by A32, FINSEQ_1:def_7; then (G1 ^ <*(F . (n + 1))*>) . m = F . m1 by A17, A33, A34, FINSEQ_1:def_7; hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m by A29, A35, PROB_2:def_2; ::_thesis: verum end; case k <> len (G1 ^ <*(F . (n + 1))*>) ; ::_thesis: (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m then k <> (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22; then A36: k <> (len G1) + 1 by FINSEQ_1:39; A37: k in Seg (len (G1 ^ <*(F . (n + 1))*>)) by A27, FINSEQ_1:def_3; then k in Seg ((len G1) + (len <*(F . (n + 1))*>)) by FINSEQ_1:22; then k in Seg ((len G1) + 1) by FINSEQ_1:39; then k <= (len G1) + 1 by FINSEQ_1:1; then k < (len G1) + 1 by A36, XXREAL_0:1; then A38: k <= len G1 by NAT_1:13; 1 <= k by A37, FINSEQ_1:1; then A39: k in dom G1 by A38, FINSEQ_3:25; then A40: (G1 ^ <*(F . (n + 1))*>) . k = G1 . k by FINSEQ_1:def_7; now__::_thesis:_(_(_m_=_len_(G1_^_<*(F_._(n_+_1))*>)_&_(G1_^_<*(F_._(n_+_1))*>)_._k_misses_(G1_^_<*(F_._(n_+_1))*>)_._m_)_or_(_m_<>_len_(G1_^_<*(F_._(n_+_1))*>)_&_(G1_^_<*(F_._(n_+_1))*>)_._k_misses_(G1_^_<*(F_._(n_+_1))*>)_._m_)_) percases ( m = len (G1 ^ <*(F . (n + 1))*>) or m <> len (G1 ^ <*(F . (n + 1))*>) ) ; case m = len (G1 ^ <*(F . (n + 1))*>) ; ::_thesis: (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m then m = (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22; then A41: m = (len G1) + 1 by FINSEQ_1:39; 1 <= len <*(F . (n + 1))*> by FINSEQ_1:39; then A42: (G1 ^ <*(F . (n + 1))*>) . m = <*(F . (n + 1))*> . 1 by A41, FINSEQ_1:65 .= F . (n + 1) by FINSEQ_1:def_8 ; consider k1 being Nat such that A43: k1 in dom F1 and A44: F1 . k1 = G1 . k by A7, A39; k1 in Seg (len F1) by A43, FINSEQ_1:def_3; then k1 <= n by A5, FINSEQ_1:1; then A45: k1 <> n + 1 by NAT_1:13; (G1 ^ <*(F . (n + 1))*>) . k = F . k1 by A17, A40, A43, A44, FINSEQ_1:def_7; hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m by A42, A45, PROB_2:def_2; ::_thesis: verum end; case m <> len (G1 ^ <*(F . (n + 1))*>) ; ::_thesis: (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m then m <> (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22; then A46: m <> (len G1) + 1 by FINSEQ_1:39; A47: m in Seg (len (G1 ^ <*(F . (n + 1))*>)) by A27, FINSEQ_1:def_3; then m in Seg ((len G1) + (len <*(F . (n + 1))*>)) by FINSEQ_1:22; then m in Seg ((len G1) + 1) by FINSEQ_1:39; then m <= (len G1) + 1 by FINSEQ_1:1; then m < (len G1) + 1 by A46, XXREAL_0:1; then A48: m <= len G1 by NAT_1:13; 1 <= m by A47, FINSEQ_1:1; then m in dom G1 by A48, FINSEQ_3:25; then (G1 ^ <*(F . (n + 1))*>) . m = G1 . m by FINSEQ_1:def_7; hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m by A26, A40, PROB_2:def_2; ::_thesis: verum end; end; end; hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m ; ::_thesis: verum end; end; end; hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m ; ::_thesis: verum end; case ( not k in dom (G1 ^ <*(F . (n + 1))*>) or not m in dom (G1 ^ <*(F . (n + 1))*>) ) ; ::_thesis: (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m then ( (G1 ^ <*(F . (n + 1))*>) . k = {} or (G1 ^ <*(F . (n + 1))*>) . m = {} ) by FUNCT_1:def_2; hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m by XBOOLE_1:65; ::_thesis: verum end; end; end; hence (G1 ^ <*(F . (n + 1))*>) . k misses (G1 ^ <*(F . (n + 1))*>) . m ; ::_thesis: verum end; 1 <= n + 1 by NAT_1:11; then n + 1 in Seg (n + 1) by FINSEQ_1:1; then n + 1 in dom F by A3, FINSEQ_1:def_3; then F . (n + 1) in rng F by FUNCT_1:3; then <*(F . (n + 1))*> is FinSequence of S by FINSEQ_1:74; then reconsider G = G1 ^ <*(F . (n + 1))*> as Finite_Sep_Sequence of S by A25, FINSEQ_1:75, PROB_2:def_2; A49: len G = (len G1) + (len <*(F . (n + 1))*>) by FINSEQ_1:22 .= (len G1) + 1 by FINSEQ_1:39 ; A50: for k being Nat st k in dom G holds ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) proof let k be Nat; ::_thesis: ( k in dom G implies ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) ) assume A51: k in dom G ; ::_thesis: ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) reconsider k = k as Element of NAT by ORDINAL1:def_12; now__::_thesis:_(_(_k_=_len_G_&_G_._k_<>_{}_&_ex_m_being_Nat_st_ (_m_in_dom_F_&_F_._m_=_G_._k_)_)_or_(_k_<>_len_G_&_G_._k_<>_{}_&_ex_m_being_Nat_st_ (_m_in_dom_F_&_F_._m_=_G_._k_)_)_) percases ( k = len G or k <> len G ) ; caseA52: k = len G ; ::_thesis: ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) 1 <= n + 1 by NAT_1:11; then n + 1 in Seg (n + 1) by FINSEQ_1:1; then A53: n + 1 in dom F by A3, FINSEQ_1:def_3; dom <*(F . (n + 1))*> = Seg 1 by FINSEQ_1:38; then 1 in dom <*(F . (n + 1))*> by FINSEQ_1:2, TARSKI:def_1; then G . k = <*(F . (n + 1))*> . 1 by A49, A52, FINSEQ_1:def_7 .= F . (n + 1) by FINSEQ_1:def_8 ; hence ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) by A24, A53; ::_thesis: verum end; caseA54: k <> len G ; ::_thesis: ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) k <= len G by A51, FINSEQ_3:25; then k < len G by A54, XXREAL_0:1; then A55: k <= len G1 by A49, NAT_1:13; 1 <= k by A51, FINSEQ_3:25; then A56: k in dom G1 by A55, FINSEQ_3:25; then A57: G . k = G1 . k by FINSEQ_1:def_7; ex m being Nat st ( m in dom F & F . m = G . k ) proof consider m being Nat such that A58: ( m in dom F1 & F1 . m = G1 . k ) by A7, A56; take m ; ::_thesis: ( m in dom F & F . m = G . k ) dom F1 c= dom F by A8, FINSEQ_1:26; hence ( m in dom F & F . m = G . k ) by A17, A57, A58, FINSEQ_1:def_7; ::_thesis: verum end; hence ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) by A7, A56, A57; ::_thesis: verum end; end; end; hence ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) ; ::_thesis: verum end; take G = G; ::_thesis: ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) ) ) rng F = (rng F1) \/ (rng <*(F . (n + 1))*>) by A17, FINSEQ_1:31; then union (rng F) = (union (rng F1)) \/ (union (rng <*(F . (n + 1))*>)) by ZFMISC_1:78 .= union ((rng G1) \/ (rng <*(F . (n + 1))*>)) by A6, ZFMISC_1:78 .= union (rng G) by FINSEQ_1:31 ; hence ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) ) ) by A50; ::_thesis: verum end; end; end; hence ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for k being Nat st k in dom G holds ( G . k <> {} & ex m being Nat st ( m in dom F & F . m = G . k ) ) ) ) ; ::_thesis: verum end; hence ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds ( G . n <> {} & ex m being Nat st ( m in dom F & F . m = G . n ) ) ) ) ; ::_thesis: verum end; A59: len F = len F ; A60: S1[ 0 ] proof let F be Finite_Sep_Sequence of S; ::_thesis: ( len F = 0 implies ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds ( G . n <> {} & ex m being Nat st ( m in dom F & F . m = G . n ) ) ) ) ) assume A61: len F = 0 ; ::_thesis: ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds ( G . n <> {} & ex m being Nat st ( m in dom F & F . m = G . n ) ) ) ) take G = F; ::_thesis: ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds ( G . n <> {} & ex m being Nat st ( m in dom F & F . m = G . n ) ) ) ) G = {} by A61; hence ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds ( G . n <> {} & ex m being Nat st ( m in dom F & F . m = G . n ) ) ) ) ; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A60, A1); hence ex G being Finite_Sep_Sequence of S st ( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds ( G . n <> {} & ex m being Nat st ( m in dom F & F . m = G . n ) ) ) ) by A59; ::_thesis: verum end; Lm1: for a being FinSequence of ExtREAL for p, N being Element of ExtREAL st N = len a & ( for n being Nat st n in dom a holds a . n = p ) holds Sum a = N * p proof defpred S1[ Nat] means for F being FinSequence of ExtREAL for p being Element of ExtREAL st \$1 = len F & ( for n being Nat st n in dom F holds F . n = p ) holds ex N being Element of ExtREAL st ( N = \$1 & Sum F = N * p ); let a be FinSequence of ExtREAL ; ::_thesis: for p, N being Element of ExtREAL st N = len a & ( for n being Nat st n in dom a holds a . n = p ) holds Sum a = N * p let p, N be Element of ExtREAL ; ::_thesis: ( N = len a & ( for n being Nat st n in dom a holds a . n = p ) implies Sum a = N * p ) assume that A1: N = len a and A2: for n being Nat st n in dom a holds a . n = p ; ::_thesis: Sum a = N * p A3: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] reconsider k = k as Element of NAT by ORDINAL1:def_12; for F being FinSequence of ExtREAL for p being Element of ExtREAL st k + 1 = len F & ( for n being Nat st n in dom F holds F . n = p ) holds ex N being Element of ExtREAL st ( N = k + 1 & Sum F = N * p ) proof let F be FinSequence of ExtREAL ; ::_thesis: for p being Element of ExtREAL st k + 1 = len F & ( for n being Nat st n in dom F holds F . n = p ) holds ex N being Element of ExtREAL st ( N = k + 1 & Sum F = N * p ) let p be Element of ExtREAL ; ::_thesis: ( k + 1 = len F & ( for n being Nat st n in dom F holds F . n = p ) implies ex N being Element of ExtREAL st ( N = k + 1 & Sum F = N * p ) ) assume that A5: k + 1 = len F and A6: for n being Nat st n in dom F holds F . n = p ; ::_thesis: ex N being Element of ExtREAL st ( N = k + 1 & Sum F = N * p ) F <> {} by A5; then consider G being FinSequence, v being set such that A7: F = G ^ <*v*> by FINSEQ_1:46; reconsider G = G as FinSequence of ExtREAL by A7, FINSEQ_1:36; A8: k + 1 = (len G) + (len <*v*>) by A5, A7, FINSEQ_1:22 .= (len G) + 1 by FINSEQ_1:39 ; dom <*v*> = Seg 1 by FINSEQ_1:38; then A9: 1 in dom <*v*> by FINSEQ_1:2, TARSKI:def_1; 1 <= k + 1 by NAT_1:11; then A10: k + 1 in dom F by A5, FINSEQ_3:25; v = <*v*> . 1 by FINSEQ_1:40 .= F . (k + 1) by A7, A8, A9, FINSEQ_1:def_7 .= p by A6, A10 ; then reconsider v = v as Element of ExtREAL ; consider g being Function of NAT,ExtREAL such that A11: Sum G = g . (len G) and A12: g . 0 = 0. and A13: for i being Element of NAT st i < len G holds g . (i + 1) = (g . i) + (G . (i + 1)) by EXTREAL1:def_2; for n being Nat st n in dom G holds G . n = p proof let n be Nat; ::_thesis: ( n in dom G implies G . n = p ) A14: len G <= (len G) + 1 by NAT_1:11; assume A15: n in dom G ; ::_thesis: G . n = p then n <= len G by FINSEQ_3:25; then A16: n <= (len G) + 1 by A14, XXREAL_0:2; A17: len F = (len G) + (len <*v*>) by A7, FINSEQ_1:22 .= (len G) + 1 by FINSEQ_1:39 ; 1 <= n by A15, FINSEQ_3:25; then n in dom F by A16, A17, FINSEQ_3:25; then F . n = p by A6; hence G . n = p by A7, A15, FINSEQ_1:def_7; ::_thesis: verum end; then consider N1 being Element of ExtREAL such that A18: N1 = k and A19: Sum G = N1 * p by A4, A8; consider f being Function of NAT,ExtREAL such that A20: Sum F = f . (len F) and A21: f . 0 = 0. and A22: for i being Element of NAT st i < len F holds f . (i + 1) = (f . i) + (F . (i + 1)) by EXTREAL1:def_2; A23: for k1 being Nat st k1 <= len G holds f . k1 = g . k1 proof defpred S2[ Nat] means ( \$1 <= len G implies f . \$1 = g . \$1 ); A24: for k1 being Nat st S2[k1] holds S2[k1 + 1] proof let k1 be Nat; ::_thesis: ( S2[k1] implies S2[k1 + 1] ) assume A25: S2[k1] ; ::_thesis: S2[k1 + 1] reconsider k1 = k1 as Element of NAT by ORDINAL1:def_12; now__::_thesis:_(_k1_+_1_<=_len_G_implies_S2[k1_+_1]_) assume A26: k1 + 1 <= len G ; ::_thesis: S2[k1 + 1] then A27: k1 < len G by NAT_1:13; len F = (len G) + (len <*v*>) by A7, FINSEQ_1:22 .= (len G) + 1 by FINSEQ_1:39 ; then k1 < len F by A27, NAT_1:13; then A28: f . (k1 + 1) = (f . k1) + (F . (k1 + 1)) by A22; 1 <= k1 + 1 by NAT_1:11; then A29: k1 + 1 in dom G by A26, FINSEQ_3:25; ( k1 <= k1 + 1 & g . (k1 + 1) = (g . k1) + (G . (k1 + 1)) ) by A13, A27, NAT_1:11; hence S2[k1 + 1] by A7, A25, A28, A29, FINSEQ_1:def_7, XXREAL_0:2; ::_thesis: verum end; hence S2[k1 + 1] ; ::_thesis: verum end; A30: S2[ 0 ] by A21, A12; for k1 being Nat holds S2[k1] from NAT_1:sch_2(A30, A24); hence for k1 being Nat st k1 <= len G holds f . k1 = g . k1 ; ::_thesis: verum end; take N1 + 1. ; ::_thesis: ( N1 + 1. = k + 1 & Sum F = (N1 + 1.) * p ) k < len F by A5, NAT_1:13; then Sum F = (f . k) + (F . (k + 1)) by A5, A20, A22 .= (g . k) + (F . (k + 1)) by A8, A23 ; then Sum F = (Sum G) + p by A6, A8, A10, A11 .= (N1 * p) + (1. * p) by A19, XXREAL_3:81 ; hence ( N1 + 1. = k + 1 & Sum F = (N1 + 1.) * p ) by A18, SUPINF_2:1, XXREAL_3:96; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; for F being FinSequence of ExtREAL for p being Element of ExtREAL st 0 = len F & ( for n being Nat st n in dom F holds F . n = p ) holds ex N being Element of ExtREAL st ( N = 0 & Sum F = N * p ) proof let F be FinSequence of ExtREAL ; ::_thesis: for p being Element of ExtREAL st 0 = len F & ( for n being Nat st n in dom F holds F . n = p ) holds ex N being Element of ExtREAL st ( N = 0 & Sum F = N * p ) let p be Element of ExtREAL ; ::_thesis: ( 0 = len F & ( for n being Nat st n in dom F holds F . n = p ) implies ex N being Element of ExtREAL st ( N = 0 & Sum F = N * p ) ) assume that A31: 0 = len F and for n being Nat st n in dom F holds F . n = p ; ::_thesis: ex N being Element of ExtREAL st ( N = 0 & Sum F = N * p ) take 0. ; ::_thesis: ( 0. = 0 & Sum F = 0. * p ) ex f being Function of NAT,ExtREAL st ( Sum F = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds f . (i + 1) = (f . i) + (F . (i + 1)) ) ) by EXTREAL1:def_2; hence ( 0. = 0 & Sum F = 0. * p ) by A31; ::_thesis: verum end; then A32: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A32, A3); then ex N9 being Element of ExtREAL st ( N9 = len a & Sum a = N9 * p ) by A2; hence Sum a = N * p by A1; ::_thesis: verum end; Lm2: for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) & ( for x being set st x in dom f holds 0. <> f . x ) holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) & ( for x being set st x in dom f holds 0. <> f . x ) holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) & ( for x being set st x in dom f holds 0. <> f . x ) holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) let f be PartFunc of X,ExtREAL; ::_thesis: ( f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) & ( for x being set st x in dom f holds 0. <> f . x ) implies ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) ) assume that A1: f is_simple_func_in S and A2: for x being set st x in dom f holds 0. <= f . x and A3: for x being set st x in dom f holds 0. <> f . x ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) consider F1 being Finite_Sep_Sequence of S such that A4: dom f = union (rng F1) and A5: for n being Nat for x, y being Element of X st n in dom F1 & x in F1 . n & y in F1 . n holds f . x = f . y by A1, MESFUNC2:def_4; consider G being Finite_Sep_Sequence of S such that A6: union (rng F1) = union (rng G) and A7: for n being Nat st n in dom G holds ( G . n <> {} & ex m being Nat st ( m in dom F1 & F1 . m = G . n ) ) by Th13; set F = <*{}*> ^ G; ( rng <*{}*> = {{}} & {} in S ) by FINSEQ_1:38, MEASURE1:7; then rng <*{}*> c= S by ZFMISC_1:31; then (rng <*{}*>) \/ (rng G) c= S by XBOOLE_1:8; then rng (<*{}*> ^ G) c= S by FINSEQ_1:31; then reconsider F = <*{}*> ^ G as FinSequence of S by FINSEQ_1:def_4; for x, y being set st x <> y holds F . x misses F . y proof let x, y be set ; ::_thesis: ( x <> y implies F . x misses F . y ) assume A8: x <> y ; ::_thesis: F . x misses F . y now__::_thesis:_(_(_x_in_dom_F_&_y_in_dom_F_&_F_._x_misses_F_._y_)_or_(_(_not_x_in_dom_F_or_not_y_in_dom_F_)_&_F_._x_misses_F_._y_)_) percases ( ( x in dom F & y in dom F ) or not x in dom F or not y in dom F ) ; caseA9: ( x in dom F & y in dom F ) ; ::_thesis: F . x misses F . y then reconsider x = x, y = y as Element of NAT ; A10: x in Seg (len (<*{}*> ^ G)) by A9, FINSEQ_1:def_3; then A11: x <= len (<*{}*> ^ G) by FINSEQ_1:1; A12: y in Seg (len (<*{}*> ^ G)) by A9, FINSEQ_1:def_3; then A13: 1 <= y by FINSEQ_1:1; A14: y <= len (<*{}*> ^ G) by A12, FINSEQ_1:1; A15: 1 <= x by A10, FINSEQ_1:1; now__::_thesis:_(_(_(_x_=_1_or_y_=_1_)_&_F_._x_misses_F_._y_)_or_(_x_<>_1_&_y_<>_1_&_F_._x_misses_F_._y_)_) percases ( x = 1 or y = 1 or ( x <> 1 & y <> 1 ) ) ; caseA16: ( x = 1 or y = 1 ) ; ::_thesis: F . x misses F . y A17: dom <*{}*> = Seg 1 by FINSEQ_1:38; now__::_thesis:_(_(_x_=_1_&_F_._x_misses_F_._y_)_or_(_y_=_1_&_F_._x_misses_F_._y_)_) percases ( x = 1 or y = 1 ) by A16; caseA18: x = 1 ; ::_thesis: F . x misses F . y then x in dom <*{}*> by A17, FINSEQ_1:2, TARSKI:def_1; then F . x = <*{}*> . x by FINSEQ_1:def_7; then F . x = {} by A18, FINSEQ_1:def_8; hence F . x misses F . y by XBOOLE_1:65; ::_thesis: verum end; caseA19: y = 1 ; ::_thesis: F . x misses F . y then y in dom <*{}*> by A17, FINSEQ_1:2, TARSKI:def_1; then F . y = <*{}*> . y by FINSEQ_1:def_7; then F . y = {} by A19, FINSEQ_1:def_8; hence F . x misses F . y by XBOOLE_1:65; ::_thesis: verum end; end; end; hence F . x misses F . y ; ::_thesis: verum end; caseA20: ( x <> 1 & y <> 1 ) ; ::_thesis: F . x misses F . y then 1 < y by A13, XXREAL_0:1; then len <*{}*> < y by FINSEQ_1:40; then A21: F . y = G . (y - (len <*{}*>)) by A14, FINSEQ_1:24; 1 < x by A15, A20, XXREAL_0:1; then len <*{}*> < x by FINSEQ_1:40; then A22: F . x = G . (x - (len <*{}*>)) by A11, FINSEQ_1:24; x - (len <*{}*>) <> y - (len <*{}*>) by A8; hence F . x misses F . y by A22, A21, PROB_2:def_2; ::_thesis: verum end; end; end; hence F . x misses F . y ; ::_thesis: verum end; case ( not x in dom F or not y in dom F ) ; ::_thesis: F . x misses F . y then ( F . x = {} or F . y = {} ) by FUNCT_1:def_2; hence F . x misses F . y by XBOOLE_1:65; ::_thesis: verum end; end; end; hence F . x misses F . y ; ::_thesis: verum end; then reconsider F = F as Finite_Sep_Sequence of S by PROB_2:def_2; A23: union (rng F) = union ((rng <*{}*>) \/ (rng G)) by FINSEQ_1:31 .= union ({{}} \/ (rng G)) by FINSEQ_1:38 .= (union {{}}) \/ (union (rng G)) by ZFMISC_1:78 .= {} \/ (union (rng G)) by ZFMISC_1:25 .= dom f by A4, A6 ; defpred S1[ Nat, Element of ExtREAL ] means ( ( for x being Element of X st \$1 in dom F & \$1 = 1 holds \$2 = 0. ) & ( for x being Element of X st \$1 in dom F & \$1 >= 2 & x in F . \$1 holds \$2 = f . x ) ); A24: for k being Nat st k in Seg (len F) holds ex y being Element of ExtREAL st S1[k,y] proof let k be Nat; ::_thesis: ( k in Seg (len F) implies ex y being Element of ExtREAL st S1[k,y] ) assume A25: k in Seg (len F) ; ::_thesis: ex y being Element of ExtREAL st S1[k,y] ex y being Element of ExtREAL st S1[k,y] proof now__::_thesis:_(_(_k_=_1_&_ex_y_being_Element_of_ExtREAL_ex_y_being_Element_of_ExtREAL_st_S1[k,y]_)_or_(_k_<>_1_&_ex_y_being_Element_of_ExtREAL_ex_y_being_Element_of_ExtREAL_st_S1[k,y]_)_) percases ( k = 1 or k <> 1 ) ; caseA26: k = 1 ; ::_thesis: ex y being Element of ExtREAL ex y being Element of ExtREAL st S1[k,y] take y = 0. ; ::_thesis: ex y being Element of ExtREAL st S1[k,y] ( ( for x being Element of X st k in dom F & k = 1 holds y = 0. ) & ( for x being Element of X st k in dom F & k >= 2 & x in F . k holds y = f . x ) ) by A26; hence ex y being Element of ExtREAL st S1[k,y] ; ::_thesis: verum end; caseA27: k <> 1 ; ::_thesis: ex y being Element of ExtREAL ex y being Element of ExtREAL st S1[k,y] A28: k <= len F by A25, FINSEQ_1:1; then k <= (len <*{}*>) + (len G) by FINSEQ_1:22; then A29: k - (len <*{}*>) <= len G by XREAL_1:20; 1 <= k by A25, FINSEQ_1:1; then 1 < k by A27, XXREAL_0:1; then 1 + 1 <= k by NAT_1:13; then A30: (len <*{}*>) + 1 <= k by FINSEQ_1:39; then consider k2 being Nat such that A31: ((len <*{}*>) + 1) + k2 = k by NAT_1:10; reconsider k2 = k2 as Element of NAT by ORDINAL1:def_12; 1 + k2 = k - (len <*{}*>) by A31; then 1 <= 1 + k2 by A30, XREAL_1:19; then 1 + k2 in Seg (len G) by A31, A29, FINSEQ_1:1; then A32: 1 + k2 in dom G by FINSEQ_1:def_3; then consider m1 being Nat such that A33: m1 in dom F1 and A34: F1 . m1 = G . (1 + k2) by A7; k <= (len <*{}*>) + (len G) by A28, FINSEQ_1:22; then A35: F . k = G . (k - (len <*{}*>)) by A30, FINSEQ_1:23 .= G . (1 + k2) by A31 ; then F . k <> {} by A7, A32; then consider z being set such that A36: z in F . k by XBOOLE_0:def_1; take y = f . z; ::_thesis: ex y being Element of ExtREAL st S1[k,y] F . k in rng F1 by A35, A33, A34, FUNCT_1:3; then F . k in S ; then reconsider z = z as Element of X by A36; A37: for x being Element of X st k in dom F & k >= 2 & x in F . k holds y = f . x proof let x be Element of X; ::_thesis: ( k in dom F & k >= 2 & x in F . k implies y = f . x ) assume that k in dom F and k >= 2 and A38: x in F . k ; ::_thesis: y = f . x z in F1 . m1 by A35, A36, A34; hence y = f . x by A5, A35, A33, A34, A38; ::_thesis: verum end; for x being Element of X st k in dom F & k = 1 holds y = 0. by A27; hence ex y being Element of ExtREAL st S1[k,y] by A37; ::_thesis: verum end; end; end; hence ex y being Element of ExtREAL st S1[k,y] ; ::_thesis: verum end; hence ex y being Element of ExtREAL st S1[k,y] ; ::_thesis: verum end; consider a being FinSequence of ExtREAL such that A39: ( dom a = Seg (len F) & ( for n being Nat st n in Seg (len F) holds S1[n,a . n] ) ) from FINSEQ_1:sch_5(A24); A40: dom F = dom a by A39, FINSEQ_1:def_3; A41: for n being Nat for x being Element of X st n in dom F & n >= 2 & x in F . n holds a . n = f . x proof let n be Nat; ::_thesis: for x being Element of X st n in dom F & n >= 2 & x in F . n holds a . n = f . x let x be Element of X; ::_thesis: ( n in dom F & n >= 2 & x in F . n implies a . n = f . x ) assume that A42: n in dom F and A43: ( n >= 2 & x in F . n ) ; ::_thesis: a . n = f . x n in Seg (len F) by A42, FINSEQ_1:def_3; hence a . n = f . x by A39, A42, A43; ::_thesis: verum end; A44: for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) proof let n be Nat; ::_thesis: ( 2 <= n & n in dom a implies ( 0. < a . n & a . n < +infty ) ) assume that A45: 2 <= n and A46: n in dom a ; ::_thesis: ( 0. < a . n & a . n < +infty ) 1 + 1 <= n by A45; then A47: (len <*{}*>) + 1 <= n by FINSEQ_1:39; n <= len F by A39, A46, FINSEQ_1:1; then n <= (len <*{}*>) + (len G) by FINSEQ_1:22; then A48: F . n = G . (n - (len <*{}*>)) by A47, FINSEQ_1:23 .= G . (n - 1) by FINSEQ_1:39 ; ( dom <*{}*> = {1} & 1 <> n ) by A45, FINSEQ_1:2, FINSEQ_1:38; then not n in dom <*{}*> by TARSKI:def_1; then consider k being Nat such that A49: k in dom G and A50: n = (len <*{}*>) + k by A40, A46, FINSEQ_1:25; n = 1 + k by A50, FINSEQ_1:39; then F . n <> {} by A7, A48, A49; then consider x1 being set such that A51: x1 in F . n by XBOOLE_0:def_1; A52: F . n c= union (rng F) by A40, A46, FUNCT_1:3, ZFMISC_1:74; then x1 in dom f by A23, A51; then reconsider x1 = x1 as Element of X ; A53: 0. <> f . x1 by A3, A23, A51, A52; f is V73() by A1, MESFUNC2:def_4; then A54: |.(f . x1).| < +infty by A23, A51, A52, MESFUNC2:def_1; a . n = f . x1 by A41, A40, A45, A46, A51; hence ( 0. < a . n & a . n < +infty ) by A2, A23, A51, A52, A54, A53, EXTREAL2:10; ::_thesis: verum end; take F ; ::_thesis: ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) take a ; ::_thesis: ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) A55: for n9 being Nat st n9 in dom F holds for x being set st x in F . n9 holds f . x = a . n9 proof let n9 be Nat; ::_thesis: ( n9 in dom F implies for x being set st x in F . n9 holds f . x = a . n9 ) assume A56: n9 in dom F ; ::_thesis: for x being set st x in F . n9 holds f . x = a . n9 now__::_thesis:_(_(_n9_=_1_&_(_for_x_being_set_st_x_in_F_._n9_holds_ f_._x_=_a_._n9_)_)_or_(_n9_<>_1_&_(_for_x_being_set_st_x_in_F_._n9_holds_ f_._x_=_a_._n9_)_)_) percases ( n9 = 1 or n9 <> 1 ) ; caseA57: n9 = 1 ; ::_thesis: for x being set st x in F . n9 holds f . x = a . n9 thus for x being set st x in F . n9 holds f . x = a . n9 ::_thesis: verum proof let x be set ; ::_thesis: ( x in F . n9 implies f . x = a . n9 ) dom <*{}*> = {1} by FINSEQ_1:2, FINSEQ_1:38; then 1 in dom <*{}*> by TARSKI:def_1; then A58: F . 1 = <*{}*> . 1 by FINSEQ_1:def_7 .= {} by FINSEQ_1:40 ; assume x in F . n9 ; ::_thesis: f . x = a . n9 hence f . x = a . n9 by A57, A58; ::_thesis: verum end; end; caseA59: n9 <> 1 ; ::_thesis: for x being set st x in F . n9 holds f . x = a . n9 n9 in Seg (len F) by A56, FINSEQ_1:def_3; then 1 <= n9 by FINSEQ_1:1; then 1 < n9 by A59, XXREAL_0:1; then A60: 1 + 1 <= n9 by NAT_1:13; thus for x being set st x in F . n9 holds f . x = a . n9 ::_thesis: verum proof let x be set ; ::_thesis: ( x in F . n9 implies f . x = a . n9 ) assume A61: x in F . n9 ; ::_thesis: f . x = a . n9 F . n9 in rng F by A56, FUNCT_1:3; then F . n9 in S ; then reconsider x = x as Element of X by A61; a . n9 = f . x by A41, A56, A60, A61; hence f . x = a . n9 ; ::_thesis: verum end; end; end; end; hence for x being set st x in F . n9 holds f . x = a . n9 ; ::_thesis: verum end; len F = (len <*{}*>) + (len G) by FINSEQ_1:22 .= 1 + (len G) by FINSEQ_1:39 ; then 1 <= len F by NAT_1:11; then 1 in Seg (len F) by FINSEQ_1:1; hence ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) by A23, A39, A40, A55, A44, Def1; ::_thesis: verum end; Lm3: for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) & ex x being set st ( x in dom f & 0. = f . x ) holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) & ex x being set st ( x in dom f & 0. = f . x ) holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) & ex x being set st ( x in dom f & 0. = f . x ) holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) let f be PartFunc of X,ExtREAL; ::_thesis: ( f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) & ex x being set st ( x in dom f & 0. = f . x ) implies ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) ) assume that A1: f is_simple_func_in S and A2: for x being set st x in dom f holds 0. <= f . x and A3: ex x being set st ( x in dom f & 0. = f . x ) ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) consider x0 being set such that A4: x0 in dom f and A5: 0. = f . x0 by A3; reconsider x0 = x0 as Element of X by A4; consider F1 being Finite_Sep_Sequence of S such that A6: dom f = union (rng F1) and A7: for n being Nat for x, y being Element of X st n in dom F1 & x in F1 . n & y in F1 . n holds f . x = f . y by A1, MESFUNC2:def_4; consider V being set such that A8: x0 in V and A9: V in rng F1 by A4, A6, TARSKI:def_4; consider n0 being set such that A10: n0 in dom F1 and A11: V = F1 . n0 by A9, FUNCT_1:def_3; set F0 = { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds f . x = 0. ) ) } ; set G1 = union { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds f . x = 0. ) ) } ; for F9 being set st F9 in { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds f . x = 0. ) ) } holds F9 in bool X proof let F9 be set ; ::_thesis: ( F9 in { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds f . x = 0. ) ) } implies F9 in bool X ) assume F9 in { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds f . x = 0. ) ) } ; ::_thesis: F9 in bool X then ex Fn being Element of S st ( F9 = Fn & Fn in rng F1 & ( for x being Element of X st x in Fn holds f . x = 0. ) ) ; hence F9 in bool X ; ::_thesis: verum end; then reconsider F0 = { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds f . x = 0. ) ) } as Subset-Family of X by TARSKI:def_3; set N = { n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds f . x = 0. ) ) } ; A12: len F1 <= (len F1) + 1 by NAT_1:11; reconsider n0 = n0 as Element of NAT by A10; ( F1 . n0 is Element of S & F1 . n0 in rng F1 & ( for x being Element of X st x in F1 . n0 holds f . x = 0. ) ) proof F1 . n0 in rng F1 by A10, FUNCT_1:3; hence F1 . n0 is Element of S ; ::_thesis: ( F1 . n0 in rng F1 & ( for x being Element of X st x in F1 . n0 holds f . x = 0. ) ) thus F1 . n0 in rng F1 by A10, FUNCT_1:3; ::_thesis: for x being Element of X st x in F1 . n0 holds f . x = 0. let x be Element of X; ::_thesis: ( x in F1 . n0 implies f . x = 0. ) assume x in F1 . n0 ; ::_thesis: f . x = 0. hence f . x = 0. by A5, A7, A8, A10, A11; ::_thesis: verum end; then A13: F1 . n0 in F0 ; for z being set st z in F0 holds z in rng F1 proof let z be set ; ::_thesis: ( z in F0 implies z in rng F1 ) assume z in F0 ; ::_thesis: z in rng F1 then ex Fn9 being Element of S st ( z = Fn9 & Fn9 in rng F1 & ( for x being Element of X st x in Fn9 holds f . x = 0. ) ) ; hence z in rng F1 ; ::_thesis: verum end; then A14: F0 c= rng F1 by TARSKI:def_3; for z being set st z in { n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds f . x = 0. ) ) } holds z in dom F1 proof let z be set ; ::_thesis: ( z in { n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds f . x = 0. ) ) } implies z in dom F1 ) assume z in { n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds f . x = 0. ) ) } ; ::_thesis: z in dom F1 then ex n9 being Element of NAT st ( z = n9 & n9 in dom F1 & ( for x being Element of X st x in F1 . n9 holds f . x = 0. ) ) ; hence z in dom F1 ; ::_thesis: verum end; then A15: { n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds f . x = 0. ) ) } c= dom F1 by TARSKI:def_3; then reconsider N = { n where n is Element of NAT : ( n in dom F1 & ( for x being Element of X st x in F1 . n holds f . x = 0. ) ) } as finite set ; consider P1 being FinSequence such that A16: ( rng P1 = N & P1 is one-to-one ) by FINSEQ_4:58; reconsider F0 = F0 as N_Sub_set_fam of X by A14, A13; for F9 being set st F9 in F0 holds F9 in S proof let F9 be set ; ::_thesis: ( F9 in F0 implies F9 in S ) assume F9 in F0 ; ::_thesis: F9 in S then ex Fn being Element of S st ( F9 = Fn & Fn in rng F1 & ( for x being Element of X st x in Fn holds f . x = 0. ) ) ; hence F9 in S ; ::_thesis: verum end; then F0 c= S by TARSKI:def_3; then reconsider G1 = union { Fn where Fn is Element of S : ( Fn in rng F1 & ( for x being Element of X st x in Fn holds f . x = 0. ) ) } as Element of S by MEASURE1:def_5; A17: len P1 = card N by A16, FINSEQ_4:62; reconsider L = Seg (len F1) as finite set ; set M = (findom F1) \ N; consider P2 being FinSequence such that A18: rng P2 = (findom F1) \ N and A19: P2 is one-to-one by FINSEQ_4:58; A20: N c= Seg (len F1) by A15, FINSEQ_1:def_3; then card N <= card L by NAT_1:43; then len P1 <= len F1 by A17, FINSEQ_1:57; then consider lenF being Nat such that A21: (len F1) + 1 = (len P1) + lenF by A12, NAT_1:10, XXREAL_0:2; reconsider lenF = lenF as Element of NAT by ORDINAL1:def_12; (findom F1) \ N = (Seg (len F1)) \ N by FINSEQ_1:def_3; then A22: card ((findom F1) \ N) = (card (Seg (len F1))) - (card N) by A20, CARD_2:44; defpred S1[ Nat, set ] means ( ( \$1 = 1 implies \$2 = G1 ) & ( \$1 >= 2 implies ex k9 being Nat st ( k9 = \$1 - 1 & \$2 = F1 . (P2 . k9) ) ) ); len P2 = card ((findom F1) \ N) by A18, A19, FINSEQ_4:62; then A23: len P2 = (((len F1) - (len P1)) + 1) - 1 by A17, A22, FINSEQ_1:57; A24: for k being Nat st k in Seg lenF holds ex U being Element of S st S1[k,U] proof let k be Nat; ::_thesis: ( k in Seg lenF implies ex U being Element of S st S1[k,U] ) assume A25: k in Seg lenF ; ::_thesis: ex U being Element of S st S1[k,U] percases ( k = 1 or k <> 1 ) ; supposeA26: k = 1 ; ::_thesis: ex U being Element of S st S1[k,U] take G1 ; ::_thesis: S1[k,G1] thus S1[k,G1] by A26; ::_thesis: verum end; supposeA27: k <> 1 ; ::_thesis: ex U being Element of S st S1[k,U] A28: k >= 1 by A25, FINSEQ_1:1; then consider k9 being Nat such that A29: k = 1 + k9 by NAT_1:10; k > 1 by A27, A28, XXREAL_0:1; then k >= 1 + 1 by NAT_1:13; then A30: k - 1 >= 1 by XREAL_1:19; k <= lenF by A25, FINSEQ_1:1; then k - 1 <= lenF - 1 by XREAL_1:9; then k9 in Seg (len P2) by A21, A23, A29, A30, FINSEQ_1:1; then k9 in dom P2 by FINSEQ_1:def_3; then P2 . k9 in (findom F1) \ N by A18, FUNCT_1:3; then F1 . (P2 . k9) in rng F1 by FUNCT_1:3; then reconsider U = F1 . (P2 . k9) as Element of S ; take U ; ::_thesis: S1[k,U] thus S1[k,U] by A27, A29; ::_thesis: verum end; end; end; consider F being FinSequence of S such that A31: ( dom F = Seg lenF & ( for k being Nat st k in Seg lenF holds S1[k,F . k] ) ) from FINSEQ_1:sch_5(A24); defpred S2[ Nat, Element of ExtREAL ] means for y being Element of X holds ( ( y in F . \$1 implies \$2 = f . y ) & ( F . \$1 = {} implies \$2 = 1. ) ); A32: for k being Nat st k in Seg (len F) holds ex x being Element of ExtREAL st S2[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len F) implies ex x being Element of ExtREAL st S2[k,x] ) assume A33: k in Seg (len F) ; ::_thesis: ex x being Element of ExtREAL st S2[k,x] then A34: k in dom F by FINSEQ_1:def_3; now__::_thesis:_(_(_k_=_1_&_ex_x_being_Element_of_ExtREAL_ex_x_being_Element_of_ExtREAL_st_S2[k,x]_)_or_(_k_<>_1_&_ex_x_being_Element_of_ExtREAL_st_S2[k,x]_)_) percases ( k = 1 or k <> 1 ) ; caseA35: k = 1 ; ::_thesis: ex x being Element of ExtREAL ex x being Element of ExtREAL st S2[k,x] take x = 0. ; ::_thesis: ex x being Element of ExtREAL st S2[k,x] A36: F . k = G1 by A31, A34, A35; for y being Element of X holds ( ( y in F . k implies 0. = f . y ) & ( F . k = {} implies 0. = 1. ) ) proof let y be Element of X; ::_thesis: ( ( y in F . k implies 0. = f . y ) & ( F . k = {} implies 0. = 1. ) ) ( y in F . k implies 0. = f . y ) proof assume y in F . k ; ::_thesis: 0. = f . y then consider Y being set such that A37: y in Y and A38: Y in F0 by A36, TARSKI:def_4; ex Fn being Element of S st ( Y = Fn & Fn in rng F1 & ( for x being Element of X st x in Fn holds f . x = 0. ) ) by A38; hence 0. = f . y by A37; ::_thesis: verum end; hence ( ( y in F . k implies 0. = f . y ) & ( F . k = {} implies 0. = 1. ) ) by A8, A11, A13, A36, TARSKI:def_4; ::_thesis: verum end; hence ex x being Element of ExtREAL st S2[k,x] ; ::_thesis: verum end; caseA39: k <> 1 ; ::_thesis: ex x being Element of ExtREAL st S2[k,x] 1 <= k by A33, FINSEQ_1:1; then 1 < k by A39, XXREAL_0:1; then A40: 1 + 1 <= k by NAT_1:13; then consider k1 being Nat such that A41: k1 = k - 1 and A42: F . k = F1 . (P2 . k1) by A31, A34; A43: 1 <= k1 by A40, A41, XREAL_1:19; k <= lenF by A31, A34, FINSEQ_1:1; then k1 <= len P2 by A21, A23, A41, XREAL_1:9; then k1 in Seg (len P2) by A43, FINSEQ_1:1; then k1 in dom P2 by FINSEQ_1:def_3; then P2 . k1 in (findom F1) \ N by A18, FUNCT_1:3; then consider k9 being set such that A44: k9 in dom F1 and A45: F . k = F1 . k9 by A42; now__::_thesis:_(_(_F_._k_=_{}_&_ex_x_being_Element_of_ExtREAL_ex_x_being_Element_of_ExtREAL_st_S2[k,x]_)_or_(_F_._k_<>_{}_&_ex_x_being_Element_of_ExtREAL_ex_x_being_Element_of_ExtREAL_st_S2[k,x]_)_) percases ( F . k = {} or F . k <> {} ) ; caseA46: F . k = {} ; ::_thesis: ex x being Element of ExtREAL ex x being Element of ExtREAL st S2[k,x] take x = 1. ; ::_thesis: ex x being Element of ExtREAL st S2[k,x] for y being Element of X holds ( ( y in F . k implies 1. = f . y ) & ( F . k = {} implies 1. = 1. ) ) by A46; hence ex x being Element of ExtREAL st S2[k,x] ; ::_thesis: verum end; case F . k <> {} ; ::_thesis: ex x being Element of ExtREAL ex x being Element of ExtREAL st S2[k,x] then consider y1 being set such that A47: y1 in F . k by XBOOLE_0:def_1; F . k in rng F by A34, FUNCT_1:3; then F . k in S ; then reconsider y1 = y1 as Element of X by A47; take x = f . y1; ::_thesis: ex x being Element of ExtREAL st S2[k,x] for y being Element of X holds ( ( y in F . k implies x = f . y ) & ( F . k = {} implies x = 1. ) ) by A7, A44, A45, A47; hence ex x being Element of ExtREAL st S2[k,x] ; ::_thesis: verum end; end; end; hence ex x being Element of ExtREAL st S2[k,x] ; ::_thesis: verum end; end; end; hence ex x being Element of ExtREAL st S2[k,x] ; ::_thesis: verum end; consider a being FinSequence of ExtREAL such that A48: ( dom a = Seg (len F) & ( for n being Nat st n in Seg (len F) holds S2[n,a . n] ) ) from FINSEQ_1:sch_5(A32); A49: for n being Nat for x being Element of X st n in dom F & x in F . n holds a . n = f . x proof let n be Nat; ::_thesis: for x being Element of X st n in dom F & x in F . n holds a . n = f . x let x be Element of X; ::_thesis: ( n in dom F & x in F . n implies a . n = f . x ) assume that A50: n in dom F and A51: x in F . n ; ::_thesis: a . n = f . x n in Seg (len F) by A50, FINSEQ_1:def_3; hence a . n = f . x by A48, A51; ::_thesis: verum end; A52: for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n proof let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds f . x = a . n ) assume A53: n in dom F ; ::_thesis: for x being set st x in F . n holds f . x = a . n let x be set ; ::_thesis: ( x in F . n implies f . x = a . n ) assume A54: x in F . n ; ::_thesis: f . x = a . n F . n in rng F by A53, FUNCT_1:3; then F . n in S ; then reconsider x = x as Element of X by A54; a . n = f . x by A49, A53, A54; hence f . x = a . n ; ::_thesis: verum end; A55: for x being Element of X st x in F1 . n0 holds f . x = 0. by A5, A7, A8, A10, A11; A56: ( a . 1 = 0. & dom F = dom a & ( for n being Nat for x being Element of X st n in dom F & x in F . n holds a . n = f . x ) ) proof reconsider F1n0 = F1 . n0 as Element of S by A9, A11; 0 + 1 <= lenF by A21, A23, XREAL_1:19; then A57: 1 in Seg lenF by FINSEQ_1:1; then A58: 1 in Seg (len F) by A31, FINSEQ_1:def_3; A59: F . 1 = G1 by A31, A57; F1n0 in F0 by A9, A11, A55; then x0 in F . 1 by A8, A11, A59, TARSKI:def_4; hence a . 1 = 0. by A5, A48, A58; ::_thesis: ( dom F = dom a & ( for n being Nat for x being Element of X st n in dom F & x in F . n holds a . n = f . x ) ) thus dom F = dom a by A48, FINSEQ_1:def_3; ::_thesis: for n being Nat for x being Element of X st n in dom F & x in F . n holds a . n = f . x thus for n being Nat for x being Element of X st n in dom F & x in F . n holds a . n = f . x by A49; ::_thesis: verum end; A60: for n, m being Nat st n in dom F & m in dom F & n = 1 & m <> 1 holds F . n misses F . m proof let n, m be Nat; ::_thesis: ( n in dom F & m in dom F & n = 1 & m <> 1 implies F . n misses F . m ) assume that A61: n in dom F and A62: m in dom F and A63: n = 1 and A64: m <> 1 ; ::_thesis: F . n misses F . m A65: F . n = G1 by A31, A61, A63; m <= lenF by A31, A62, FINSEQ_1:1; then A66: m - 1 <= lenF - 1 by XREAL_1:9; 1 <= m by A62, FINSEQ_3:25; then 1 < m by A64, XXREAL_0:1; then A67: 1 + 1 <= m by NAT_1:13; then consider k9 being Nat such that A68: k9 = m - 1 and A69: F . m = F1 . (P2 . k9) by A31, A62; m - 1 >= 1 by A67, XREAL_1:19; then k9 in Seg (len P2) by A21, A23, A68, A66, FINSEQ_1:1; then k9 in dom P2 by FINSEQ_1:def_3; then A70: P2 . k9 in (findom F1) \ N by A18, FUNCT_1:3; then A71: not P2 . k9 in N by XBOOLE_0:def_5; (F . n) /\ (F . m) = {} proof assume (F . n) /\ (F . m) <> {} ; ::_thesis: contradiction then consider v being set such that A72: v in (F . n) /\ (F . m) by XBOOLE_0:def_1; A73: v in F . m by A72, XBOOLE_0:def_4; v in F . n by A72, XBOOLE_0:def_4; then consider Y being set such that A74: v in Y and A75: Y in F0 by A65, TARSKI:def_4; consider Fv being Element of S such that A76: Y = Fv and A77: Fv in rng F1 and A78: for x being Element of X st x in Fv holds f . x = 0. by A75; consider n9 being set such that A79: n9 in dom F1 and A80: Fv = F1 . n9 by A77, FUNCT_1:def_3; reconsider n9 = n9 as Element of NAT by A79; n9 <> P2 . k9 by A70, A71, A78, A80; then F1 . n9 misses F1 . (P2 . k9) by PROB_2:def_2; then (F1 . n9) /\ (F1 . (P2 . k9)) = {} by XBOOLE_0:def_7; hence contradiction by A69, A73, A74, A76, A80, XBOOLE_0:def_4; ::_thesis: verum end; hence F . n misses F . m by XBOOLE_0:def_7; ::_thesis: verum end; A81: for n, m being Nat st n in dom F & m in dom F & n <> 1 & m <> 1 & n <> m holds F . n misses F . m proof let n, m be Nat; ::_thesis: ( n in dom F & m in dom F & n <> 1 & m <> 1 & n <> m implies F . n misses F . m ) assume that A82: n in dom F and A83: m in dom F and A84: n <> 1 and A85: m <> 1 and A86: n <> m ; ::_thesis: F . n misses F . m n <= lenF by A31, A82, FINSEQ_1:1; then A87: n - 1 <= lenF - 1 by XREAL_1:9; m <= lenF by A31, A83, FINSEQ_1:1; then A88: m - 1 <= lenF - 1 by XREAL_1:9; 1 <= m by A31, A83, FINSEQ_1:1; then 1 < m by A85, XXREAL_0:1; then A89: 1 + 1 <= m by NAT_1:13; then consider k2 being Nat such that A90: k2 = m - 1 and A91: F . m = F1 . (P2 . k2) by A31, A83; 1 <= m - 1 by A89, XREAL_1:19; then k2 in Seg (len P2) by A21, A23, A90, A88, FINSEQ_1:1; then A92: k2 in dom P2 by FINSEQ_1:def_3; 1 <= n by A31, A82, FINSEQ_1:1; then 1 < n by A84, XXREAL_0:1; then A93: 1 + 1 <= n by NAT_1:13; then consider k1 being Nat such that A94: k1 = n - 1 and A95: F . n = F1 . (P2 . k1) by A31, A82; 1 <= n - 1 by A93, XREAL_1:19; then k1 in Seg (len P2) by A21, A23, A94, A87, FINSEQ_1:1; then A96: k1 in dom P2 by FINSEQ_1:def_3; k1 <> k2 by A86, A94, A90; then P2 . k1 <> P2 . k2 by A19, A96, A92, FUNCT_1:def_4; hence F . n misses F . m by A95, A91, PROB_2:def_2; ::_thesis: verum end; A97: for x, y being set st x <> y holds F . x misses F . y proof let x, y be set ; ::_thesis: ( x <> y implies F . x misses F . y ) assume A98: x <> y ; ::_thesis: F . x misses F . y now__::_thesis:_(_(_x_in_dom_F_&_y_in_dom_F_&_F_._x_misses_F_._y_)_or_(_(_not_x_in_dom_F_or_not_y_in_dom_F_)_&_F_._x_misses_F_._y_)_) percases ( ( x in dom F & y in dom F ) or not x in dom F or not y in dom F ) ; caseA99: ( x in dom F & y in dom F ) ; ::_thesis: F . x misses F . y then reconsider x = x, y = y as Element of NAT ; now__::_thesis:_(_(_(_x_=_1_or_y_=_1_)_&_F_._x_misses_F_._y_)_or_(_x_<>_1_&_y_<>_1_&_F_._x_misses_F_._y_)_) percases ( x = 1 or y = 1 or ( x <> 1 & y <> 1 ) ) ; case ( x = 1 or y = 1 ) ; ::_thesis: F . x misses F . y hence F . x misses F . y by A60, A98, A99; ::_thesis: verum end; case ( x <> 1 & y <> 1 ) ; ::_thesis: F . x misses F . y hence F . x misses F . y by A81, A98, A99; ::_thesis: verum end; end; end; hence F . x misses F . y ; ::_thesis: verum end; caseA100: ( not x in dom F or not y in dom F ) ; ::_thesis: F . x misses F . y now__::_thesis:_(_(_not_x_in_dom_F_&_F_._x_misses_F_._y_)_or_(_not_y_in_dom_F_&_F_._x_misses_F_._y_)_) percases ( not x in dom F or not y in dom F ) by A100; case not x in dom F ; ::_thesis: F . x misses F . y then F . x = {} by FUNCT_1:def_2; hence F . x misses F . y by XBOOLE_1:65; ::_thesis: verum end; case not y in dom F ; ::_thesis: F . x misses F . y then F . y = {} by FUNCT_1:def_2; hence F . x misses F . y by XBOOLE_1:65; ::_thesis: verum end; end; end; hence F . x misses F . y ; ::_thesis: verum end; end; end; hence F . x misses F . y ; ::_thesis: verum end; for z being set st z in union (rng F) holds z in union (rng F1) proof let z be set ; ::_thesis: ( z in union (rng F) implies z in union (rng F1) ) assume z in union (rng F) ; ::_thesis: z in union (rng F1) then consider Y being set such that A101: z in Y and A102: Y in rng F by TARSKI:def_4; consider k being set such that A103: k in dom F and A104: Y = F . k by A102, FUNCT_1:def_3; reconsider k = k as Element of NAT by A103; now__::_thesis:_(_(_k_=_1_&_z_in_union_(rng_F1)_)_or_(_k_<>_1_&_z_in_union_(rng_F1)_)_) percases ( k = 1 or k <> 1 ) ; case k = 1 ; ::_thesis: z in union (rng F1) then z in G1 by A31, A101, A103, A104; then consider Y9 being set such that A105: z in Y9 and A106: Y9 in F0 by TARSKI:def_4; ex Fn9 being Element of S st ( Y9 = Fn9 & Fn9 in rng F1 & ( for x being Element of X st x in Fn9 holds f . x = 0. ) ) by A106; hence z in union (rng F1) by A105, TARSKI:def_4; ::_thesis: verum end; caseA107: k <> 1 ; ::_thesis: z in union (rng F1) 1 <= k by A31, A103, FINSEQ_1:1; then 1 < k by A107, XXREAL_0:1; then A108: 1 + 1 <= k by NAT_1:13; then consider k9 being Nat such that A109: k9 = k - 1 and A110: F . k = F1 . (P2 . k9) by A31, A103; A111: 1 <= k9 by A108, A109, XREAL_1:19; k <= lenF by A31, A103, FINSEQ_1:1; then k9 <= len P2 by A21, A23, A109, XREAL_1:9; then k9 in dom P2 by A111, FINSEQ_3:25; then P2 . k9 in (findom F1) \ N by A18, FUNCT_1:3; then F1 . (P2 . k9) in rng F1 by FUNCT_1:3; hence z in union (rng F1) by A101, A104, A110, TARSKI:def_4; ::_thesis: verum end; end; end; hence z in union (rng F1) ; ::_thesis: verum end; then A112: union (rng F) c= union (rng F1) by TARSKI:def_3; for z being set st z in union (rng F1) holds z in union (rng F) proof let z be set ; ::_thesis: ( z in union (rng F1) implies z in union (rng F) ) assume z in union (rng F1) ; ::_thesis: z in union (rng F) then consider Y being set such that A113: z in Y and A114: Y in rng F1 by TARSKI:def_4; consider m1 being set such that A115: m1 in dom F1 and A116: Y = F1 . m1 by A114, FUNCT_1:def_3; reconsider m1 = m1 as Element of NAT by A115; now__::_thesis:_(_(_m1_in_N_&_z_in_union_(rng_F)_)_or_(_not_m1_in_N_&_z_in_union_(rng_F)_)_) percases ( m1 in N or not m1 in N ) ; case m1 in N ; ::_thesis: z in union (rng F) then ex m19 being Element of NAT st ( m1 = m19 & m19 in dom F1 & ( for x being Element of X st x in F1 . m19 holds f . x = 0. ) ) ; then Y in F0 by A114, A116; then A117: z in union F0 by A113, TARSKI:def_4; lenF >= 1 + 0 by A21, A23, XREAL_1:19; then A118: 1 in Seg lenF by FINSEQ_1:1; then F . 1 in rng F by A31, FUNCT_1:3; then union F0 in rng F by A31, A118; hence z in union (rng F) by A117, TARSKI:def_4; ::_thesis: verum end; case not m1 in N ; ::_thesis: z in union (rng F) then m1 in (findom F1) \ N by A115, XBOOLE_0:def_5; then consider m19 being set such that A119: m19 in dom P2 and A120: m1 = P2 . m19 by A18, FUNCT_1:def_3; reconsider m19 = m19 as Element of NAT by A119; A121: m19 in Seg (len P2) by A119, FINSEQ_1:def_3; then m19 <= len P2 by FINSEQ_1:1; then A122: m19 + 1 <= lenF by A21, A23, XREAL_1:6; reconsider m2 = m19 + 1 as Nat ; 1 <= m19 by A121, FINSEQ_1:1; then A123: 1 + 1 <= m19 + 1 by XREAL_1:6; then 1 <= m2 by XXREAL_0:2; then A124: m2 in Seg lenF by A122, FINSEQ_1:1; then A125: F . m2 in rng F by A31, FUNCT_1:3; ex k9 being Nat st ( k9 = m2 - 1 & F . m2 = F1 . (P2 . k9) ) by A31, A123, A124; hence z in union (rng F) by A113, A116, A120, A125, TARSKI:def_4; ::_thesis: verum end; end; end; hence z in union (rng F) ; ::_thesis: verum end; then union (rng F1) c= union (rng F) by TARSKI:def_3; then A126: union (rng F) = dom f by A6, A112, XBOOLE_0:def_10; reconsider F = F as Finite_Sep_Sequence of S by A97, PROB_2:def_2; take F ; ::_thesis: ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) take a ; ::_thesis: ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) proof A127: f is V73() by A1, MESFUNC2:def_4; 0 + 1 <= lenF by A21, A23, XREAL_1:19; then A128: 1 in dom F by A31, FINSEQ_1:1; let n be Nat; ::_thesis: ( 2 <= n & n in dom a implies ( 0. < a . n & a . n < +infty ) ) assume that A129: 2 <= n and A130: n in dom a ; ::_thesis: ( 0. < a . n & a . n < +infty ) 1 + 1 <= n by A129; then A131: 1 <= n - 1 by XREAL_1:19; consider k1 being Nat such that A132: k1 = n - 1 and A133: F . n = F1 . (P2 . k1) by A31, A56, A129, A130; n <= lenF by A31, A56, A130, FINSEQ_1:1; then n - 1 <= lenF - 1 by XREAL_1:9; then k1 in Seg (len P2) by A21, A23, A132, A131, FINSEQ_1:1; then k1 in dom P2 by FINSEQ_1:def_3; then P2 . k1 in (findom F1) \ N by A18, FUNCT_1:3; then A134: F . n in rng F1 by A133, FUNCT_1:3; n <> 1 by A129; then F . 1 misses F . n by A56, A60, A130, A128; then A135: G1 misses F . n by A31, A128; ( a . n <> 0. & 0. <= a . n & a . n < +infty ) proof percases ( F . n <> {} or F . n = {} ) ; supposeA136: F . n <> {} ; ::_thesis: ( a . n <> 0. & 0. <= a . n & a . n < +infty ) A137: F . n in rng F by A56, A130, FUNCT_1:3; then reconsider Fn = F . n as Element of S ; consider y being set such that A138: y in F . n by A136, XBOOLE_0:def_1; F . n in S by A137; then reconsider y = y as Element of X by A138; A139: a . n = f . y by A48, A130, A138; G1 /\ (F . n) = {} by A135, XBOOLE_0:def_7; then A140: not y in G1 by A138, XBOOLE_0:def_4; thus a . n <> 0. ::_thesis: ( 0. <= a . n & a . n < +infty ) proof assume a . n = 0. ; ::_thesis: contradiction then for x being Element of X st x in F . n holds f . x = 0. by A56, A130; then Fn in F0 by A134; hence contradiction by A138, A140, TARSKI:def_4; ::_thesis: verum end; A141: y in union (rng F) by A138, A137, TARSKI:def_4; then |.(f . y).| < +infty by A6, A112, A127, MESFUNC2:def_1; hence ( 0. <= a . n & a . n < +infty ) by A2, A6, A112, A139, A141, EXTREAL2:10; ::_thesis: verum end; supposeA142: F . n = {} ; ::_thesis: ( a . n <> 0. & 0. <= a . n & a . n < +infty ) hence a . n <> 0. by A48, A130; ::_thesis: ( 0. <= a . n & a . n < +infty ) thus 0. <= a . n by A48, A130, A142; ::_thesis: a . n < +infty S2[n,a . n] by A48, A130; hence a . n < +infty by A142, XXREAL_0:9; ::_thesis: verum end; end; end; hence ( 0. < a . n & a . n < +infty ) ; ::_thesis: verum end; hence ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) by A126, A56, A52, Def1; ::_thesis: verum end; theorem Th14: :: MESFUNC3:14 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) let f be PartFunc of X,ExtREAL; ::_thesis: ( f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) implies ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) ) assume A1: ( f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) ) ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) percases ( ex x being set st ( x in dom f & 0. = f . x ) or for x being set st x in dom f holds 0. <> f . x ) ; suppose ex x being set st ( x in dom f & 0. = f . x ) ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) hence ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) by A1, Lm3; ::_thesis: verum end; suppose for x being set st x in dom f holds 0. <> f . x ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) hence ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) by A1, Lm2; ::_thesis: verum end; end; end; theorem :: MESFUNC3:15 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for F being Finite_Sep_Sequence of S for a being FinSequence of ExtREAL for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for F being Finite_Sep_Sequence of S for a being FinSequence of ExtREAL for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for F being Finite_Sep_Sequence of S for a being FinSequence of ExtREAL for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) let f be PartFunc of X,ExtREAL; ::_thesis: for F being Finite_Sep_Sequence of S for a being FinSequence of ExtREAL for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) let F be Finite_Sep_Sequence of S; ::_thesis: for a being FinSequence of ExtREAL for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) let a be FinSequence of ExtREAL ; ::_thesis: for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) let x be Element of X; ::_thesis: ( F,a are_Re-presentation_of f & x in dom f implies ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) ) assume that A1: F,a are_Re-presentation_of f and A2: x in dom f ; ::_thesis: ex ax being FinSequence of ExtREAL st ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) A3: dom F = dom a by A1, Def1; deffunc H1( Nat) -> Element of ExtREAL = (a . \$1) * ((chi ((F . \$1),X)) . x); consider ax being FinSequence of ExtREAL such that A4: ( len ax = len a & ( for j being Nat st j in dom ax holds ax . j = H1(j) ) ) from FINSEQ_2:sch_1(); A5: dom ax = Seg (len a) by A4, FINSEQ_1:def_3; A6: dom f = union (rng F) by A1, Def1; A7: f . x = Sum ax proof consider Y being set such that A8: x in Y and A9: Y in rng F by A2, A6, TARSKI:def_4; consider k being set such that A10: k in dom F and A11: Y = F . k by A9, FUNCT_1:def_3; reconsider k = k as Element of NAT by A10; A12: k in Seg (len a) by A3, A10, FINSEQ_1:def_3; then A13: len ax >= k by A4, FINSEQ_1:1; A14: for i being Nat st i in Seg (len ax) & i <> k holds ax . i = 0. proof let i be Nat; ::_thesis: ( i in Seg (len ax) & i <> k implies ax . i = 0. ) assume that A15: i in Seg (len ax) and A16: i <> k ; ::_thesis: ax . i = 0. F . i misses F . k by A16, PROB_2:def_2; then (F . i) /\ (F . k) = {} by XBOOLE_0:def_7; then not x in F . i by A8, A11, XBOOLE_0:def_4; then A17: (chi ((F . i),X)) . x = 0. by FUNCT_3:def_3; ax . i = (a . i) * ((chi ((F . i),X)) . x) by A4, A5, A15; hence ax . i = 0. by A17; ::_thesis: verum end; consider SA being Function of NAT,ExtREAL such that A18: Sum ax = SA . (len ax) and A19: SA . 0 = 0. and A20: for i being Element of NAT st i < len ax holds SA . (i + 1) = (SA . i) + (ax . (i + 1)) by EXTREAL1:def_2; defpred S1[ Nat] means ( \$1 <= len ax implies ( ( \$1 < k implies SA . \$1 = 0. ) & ( \$1 >= k implies SA . \$1 = f . x ) ) ); A21: for i being Nat st i in Seg (len ax) & i = k holds ax . i = f . x proof let i be Nat; ::_thesis: ( i in Seg (len ax) & i = k implies ax . i = f . x ) assume that A22: i in Seg (len ax) and A23: i = k ; ::_thesis: ax . i = f . x (chi ((F . i),X)) . x = 1. by A8, A11, A23, FUNCT_3:def_3; then ax . i = (a . i) * 1. by A4, A5, A22 .= a . i by XXREAL_3:81 ; hence ax . i = f . x by A1, A8, A10, A11, A23, Def1; ::_thesis: verum end; A24: for i being Nat st S1[i] holds S1[i + 1] proof let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A25: S1[i] ; ::_thesis: S1[i + 1] assume A26: i + 1 <= len ax ; ::_thesis: ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) reconsider i = i as Element of NAT by ORDINAL1:def_12; now__::_thesis:_(_(_i_+_1_<_k_&_(_i_+_1_<_k_implies_SA_._(i_+_1)_=_0._)_&_(_i_+_1_>=_k_implies_SA_._(i_+_1)_=_f_._x_)_)_or_(_i_+_1_>=_k_&_(_i_+_1_<_k_implies_SA_._(i_+_1)_=_0._)_&_(_i_+_1_>=_k_implies_SA_._(i_+_1)_=_f_._x_)_)_) percases ( i + 1 < k or i + 1 >= k ) ; caseA27: i + 1 < k ; ::_thesis: ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) A28: k <= len a by A12, FINSEQ_1:1; A29: i <= i + 1 by NAT_1:11; then i < k by A27, XXREAL_0:2; then A30: i < len ax by A4, A28, XXREAL_0:2; then ( 1 <= i + 1 & i + 1 <= len ax ) by NAT_1:11, NAT_1:13; then A31: i + 1 in Seg (len ax) by FINSEQ_1:1; SA . (i + 1) = 0. + (ax . (i + 1)) by A20, A25, A27, A29, A30, XXREAL_0:2 .= ax . (i + 1) by XXREAL_3:4 .= 0. by A14, A27, A31 ; hence ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) by A27; ::_thesis: verum end; caseA32: i + 1 >= k ; ::_thesis: ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) now__::_thesis:_(_(_k_=_i_+_1_&_SA_._(i_+_1)_=_f_._x_)_or_(_k_<>_i_+_1_&_SA_._(i_+_1)_=_f_._x_)_) percases ( k = i + 1 or k <> i + 1 ) ; caseA33: k = i + 1 ; ::_thesis: SA . (i + 1) = f . x A34: k <= len a by A12, FINSEQ_1:1; then i < len ax by A4, A33, NAT_1:13; hence SA . (i + 1) = (SA . i) + (ax . (i + 1)) by A20 .= ax . k by A4, A25, A33, A34, NAT_1:13, XXREAL_3:4 .= f . x by A4, A12, A21 ; ::_thesis: verum end; case k <> i + 1 ; ::_thesis: SA . (i + 1) = f . x then A35: k < i + 1 by A32, XXREAL_0:1; 1 <= i + 1 by NAT_1:11; then A36: i + 1 in Seg (len ax) by A26, FINSEQ_1:1; i < len ax by A26, NAT_1:13; hence SA . (i + 1) = (SA . i) + (ax . (i + 1)) by A20 .= (f . x) + 0. by A14, A25, A26, A35, A36, NAT_1:13 .= f . x by XXREAL_3:4 ; ::_thesis: verum end; end; end; hence ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) by A32; ::_thesis: verum end; end; end; hence ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) ; ::_thesis: verum end; A37: S1[ 0 ] by A12, A19, FINSEQ_1:1; for i being Nat holds S1[i] from NAT_1:sch_2(A37, A24); hence f . x = Sum ax by A18, A13; ::_thesis: verum end; take ax ; ::_thesis: ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) dom ax = Seg (len a) by A4, FINSEQ_1:def_3; hence ( dom ax = dom a & ( for n being Nat st n in dom ax holds ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) by A4, A7, FINSEQ_1:def_3; ::_thesis: verum end; theorem :: MESFUNC3:16 for p being FinSequence of ExtREAL for q being FinSequence of REAL st p = q holds Sum p = Sum q by Th2; theorem Th17: :: MESFUNC3:17 for p being FinSequence of ExtREAL st not -infty in rng p & +infty in rng p holds Sum p = +infty proof let p be FinSequence of ExtREAL ; ::_thesis: ( not -infty in rng p & +infty in rng p implies Sum p = +infty ) assume A0: not -infty in rng p ; ::_thesis: ( not +infty in rng p or Sum p = +infty ) assume +infty in rng p ; ::_thesis: Sum p = +infty then ex n being set st ( n in dom p & p . n = +infty ) by FUNCT_1:def_3; then consider m being Nat such that A3: m in dom p and A4: p . m = +infty ; m in Seg (len p) by A3, FINSEQ_1:def_3; then A5: len p >= m by FINSEQ_1:1; consider f being Function of NAT,ExtREAL such that A6: Sum p = f . (len p) and A7: f . 0 = 0. and A8: for i being Element of NAT st i < len p holds f . (i + 1) = (f . i) + (p . (i + 1)) by EXTREAL1:def_2; A1: for n being Nat st n in dom p holds -infty < p . n proof let n be Nat; ::_thesis: ( n in dom p implies -infty < p . n ) assume n in dom p ; ::_thesis: -infty < p . n then p . n in rng p by FUNCT_1:def_3; hence -infty < p . n by A0, XXREAL_0:6; ::_thesis: verum end; defpred S1[ Nat] means ( \$1 <= len p implies ( ( \$1 < m implies -infty < f . \$1 ) & ( \$1 >= m implies f . \$1 = +infty ) ) ); A9: for i being Nat st S1[i] holds S1[i + 1] proof let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A10: S1[i] ; ::_thesis: S1[i + 1] assume A11: i + 1 <= len p ; ::_thesis: ( ( i + 1 < m implies -infty < f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) ) reconsider i = i as Element of NAT by ORDINAL1:def_12; B01: i < len p by A11, NAT_1:13; now__::_thesis:_(_(_i_+_1_<_m_&_-infty_<_f_._(i_+_1)_)_or_(_i_+_1_>=_m_&_(_i_+_1_<_m_implies_-infty_<_f_._(i_+_1)_)_&_(_i_+_1_>=_m_implies_f_._(i_+_1)_=_+infty_)_)_) percases ( i + 1 < m or i + 1 >= m ) ; case i + 1 < m ; ::_thesis: -infty < f . (i + 1) 1 <= i + 1 by NAT_1:11; then i + 1 in Seg (len p) by A11, FINSEQ_1:1; then i + 1 in dom p by FINSEQ_1:def_3; then A13: -infty < p . (i + 1) by A1; B02: -infty + -infty = -infty by XXREAL_3:def_2; -infty + -infty < (f . i) + (p . (i + 1)) by A10, A11, NAT_1:13, A13, XXREAL_3:64; hence -infty < f . (i + 1) by A8, B01, B02; ::_thesis: verum end; caseA14: i + 1 >= m ; ::_thesis: ( ( i + 1 < m implies -infty < f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) ) now__::_thesis:_(_(_i_+_1_=_m_&_f_._(i_+_1)_=_+infty_)_or_(_i_+_1_<>_m_&_f_._(i_+_1)_=_+infty_)_) percases ( i + 1 = m or i + 1 <> m ) ; caseA15: i + 1 = m ; ::_thesis: f . (i + 1) = +infty f . (i + 1) = (f . i) + (p . (i + 1)) by A8, B01; hence f . (i + 1) = +infty by A4, A10, A11, A15, NAT_1:13, XXREAL_3:def_2; ::_thesis: verum end; caseA16: i + 1 <> m ; ::_thesis: f . (i + 1) = +infty i < len p by A11, NAT_1:13; then A17: f . (i + 1) = (f . i) + (p . (i + 1)) by A8; 1 <= i + 1 by NAT_1:11; then i + 1 in Seg (len p) by A11, FINSEQ_1:1; then i + 1 in dom p by FINSEQ_1:def_3; then A18: p . (i + 1) <> -infty by A1; i + 1 > m by A14, A16, XXREAL_0:1; hence f . (i + 1) = +infty by A10, A11, A18, A17, NAT_1:13, XXREAL_3:def_2; ::_thesis: verum end; end; end; hence ( ( i + 1 < m implies -infty < f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) ) ; ::_thesis: verum end; end; end; hence ( ( i + 1 < m implies -infty < f . (i + 1) ) & ( i + 1 >= m implies f . (i + 1) = +infty ) ) ; ::_thesis: verum end; A19: S1[ 0 ] by A3, A7, FINSEQ_3:25; for i being Nat holds S1[i] from NAT_1:sch_2(A19, A9); hence Sum p = +infty by A6, A5; ::_thesis: verum end; definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let f be PartFunc of X,ExtREAL; assume A1: ( f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) ) ; func integral (X,S,M,f) -> Element of ExtREAL means :: MESFUNC3:def 2 ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & it = Sum x ); existence ex b1 being Element of ExtREAL ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & b1 = Sum x ) proof consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that A2: ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) ) by A1, Th14; defpred S1[ set ] means \$1 in dom F; deffunc H1( set ) -> Element of ExtREAL = (a . \$1) * ((M * F) . \$1); A3: for x being set st S1[x] holds H1(x) in ExtREAL ; consider p being PartFunc of NAT,ExtREAL such that A4: ( ( for x being set holds ( x in dom p iff ( x in NAT & S1[x] ) ) ) & ( for x being set st x in dom p holds p . x = H1(x) ) ) from PARTFUN1:sch_3(A3); for x being set st x in dom F holds x in dom p by A4; then A5: dom F c= dom p by TARSKI:def_3; for x being set st x in dom p holds x in dom F by A4; then dom p c= dom F by TARSKI:def_3; then A6: dom p = dom F by A5, XBOOLE_0:def_10; then dom p = Seg (len F) by FINSEQ_1:def_3; then A7: p is FinSequence by FINSEQ_1:def_2; rng p c= ExtREAL ; then reconsider p = p as FinSequence of ExtREAL by A7, FINSEQ_1:def_4; take Sum p ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & Sum p = Sum x ) for n being Nat st n in dom p holds p . n = (a . n) * ((M * F) . n) by A4; hence ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & Sum p = Sum x ) by A2, A6; ::_thesis: verum end; uniqueness for b1, b2 being Element of ExtREAL st ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & b1 = Sum x ) & ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & b2 = Sum x ) holds b1 = b2 proof let s1, s2 be Element of ExtREAL ; ::_thesis: ( ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & s1 = Sum x ) & ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & s2 = Sum x ) implies s1 = s2 ) assume that A8: ex F1 being Finite_Sep_Sequence of S ex a1, x1 being FinSequence of ExtREAL st ( F1,a1 are_Re-presentation_of f & a1 . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a1 holds ( 0. < a1 . n & a1 . n < +infty ) ) & dom x1 = dom F1 & ( for n being Nat st n in dom x1 holds x1 . n = (a1 . n) * ((M * F1) . n) ) & s1 = Sum x1 ) and A9: ex F2 being Finite_Sep_Sequence of S ex a2, x2 being FinSequence of ExtREAL st ( F2,a2 are_Re-presentation_of f & a2 . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a2 holds ( 0. < a2 . n & a2 . n < +infty ) ) & dom x2 = dom F2 & ( for n being Nat st n in dom x2 holds x2 . n = (a2 . n) * ((M * F2) . n) ) & s2 = Sum x2 ) ; ::_thesis: s1 = s2 thus s1 = s2 ::_thesis: verum proof consider F2 being Finite_Sep_Sequence of S, a2, x2 being FinSequence of ExtREAL such that A10: F2,a2 are_Re-presentation_of f and A11: a2 . 1 = 0. and A12: for n being Nat st 2 <= n & n in dom a2 holds ( 0. < a2 . n & a2 . n < +infty ) and A13: dom x2 = dom F2 and A14: for n being Nat st n in dom x2 holds x2 . n = (a2 . n) * ((M * F2) . n) and A15: s2 = Sum x2 by A9; A16: dom F2 = dom a2 by A10, Def1; A17: for n being Nat st n in dom a2 holds 0. <= a2 . n proof let n be Nat; ::_thesis: ( n in dom a2 implies 0. <= a2 . n ) assume A18: n in dom a2 ; ::_thesis: 0. <= a2 . n now__::_thesis:_(_(_n_=_1_&_a2_._1_=_0._)_or_(_n_<>_1_&_0._<=_a2_._n_)_) percases ( n = 1 or n <> 1 ) ; case n = 1 ; ::_thesis: a2 . 1 = 0. thus a2 . 1 = 0. by A11; ::_thesis: verum end; caseA19: n <> 1 ; ::_thesis: 0. <= a2 . n n in Seg (len a2) by A18, FINSEQ_1:def_3; then 1 <= n by FINSEQ_1:1; then 1 < n by A19, XXREAL_0:1; then 1 + 1 < n + 1 by XREAL_1:8; then 2 <= n by NAT_1:13; hence 0. <= a2 . n by A12, A18; ::_thesis: verum end; end; end; hence 0. <= a2 . n ; ::_thesis: verum end; A20: for n being Nat st n in dom F2 holds 0. <= (M * F2) . n proof let n be Nat; ::_thesis: ( n in dom F2 implies 0. <= (M * F2) . n ) assume n in dom F2 ; ::_thesis: 0. <= (M * F2) . n then ( (M * F2) . n = M . (F2 . n) & F2 . n in rng F2 ) by FUNCT_1:3, FUNCT_1:13; hence 0. <= (M * F2) . n by SUPINF_2:39; ::_thesis: verum end; A21: not -infty in rng x2 proof assume -infty in rng x2 ; ::_thesis: contradiction then consider n being set such that A22: n in dom x2 and A23: x2 . n = -infty by FUNCT_1:def_3; ( 0. <= a2 . n & 0. <= (M * F2) . n ) by A13, A16, A20, A17, A22; then 0. <= (a2 . n) * ((M * F2) . n) ; hence contradiction by A14, A22, A23; ::_thesis: verum end; consider F1 being Finite_Sep_Sequence of S, a1, x1 being FinSequence of ExtREAL such that A23: F1,a1 are_Re-presentation_of f and A24: a1 . 1 = 0. and A25: for n being Nat st 2 <= n & n in dom a1 holds ( 0. < a1 . n & a1 . n < +infty ) and A26: dom x1 = dom F1 and A27: for n being Nat st n in dom x1 holds x1 . n = (a1 . n) * ((M * F1) . n) and A28: s1 = Sum x1 by A8; A29: dom F1 = dom a1 by A23, Def1; A30: for n being Nat st n in dom a1 holds 0. <= a1 . n proof let n be Nat; ::_thesis: ( n in dom a1 implies 0. <= a1 . n ) assume A31: n in dom a1 ; ::_thesis: 0. <= a1 . n now__::_thesis:_(_(_n_=_1_&_a1_._1_=_0._)_or_(_n_<>_1_&_0._<=_a1_._n_)_) percases ( n = 1 or n <> 1 ) ; case n = 1 ; ::_thesis: a1 . 1 = 0. thus a1 . 1 = 0. by A24; ::_thesis: verum end; caseA32: n <> 1 ; ::_thesis: 0. <= a1 . n n in Seg (len a1) by A31, FINSEQ_1:def_3; then 1 <= n by FINSEQ_1:1; then 1 < n by A32, XXREAL_0:1; then 1 + 1 < n + 1 by XREAL_1:8; then 2 <= n by NAT_1:13; hence 0. <= a1 . n by A25, A31; ::_thesis: verum end; end; end; hence 0. <= a1 . n ; ::_thesis: verum end; A33: for n being Nat st n in dom F1 holds 0. <= (M * F1) . n proof let n be Nat; ::_thesis: ( n in dom F1 implies 0. <= (M * F1) . n ) assume n in dom F1 ; ::_thesis: 0. <= (M * F1) . n then ( (M * F1) . n = M . (F1 . n) & F1 . n in rng F1 ) by FUNCT_1:3, FUNCT_1:13; hence 0. <= (M * F1) . n by SUPINF_2:39; ::_thesis: verum end; A34: not -infty in rng x1 proof assume -infty in rng x1 ; ::_thesis: contradiction then consider n being set such that A35: n in dom x1 and A36: x1 . n = -infty by FUNCT_1:def_3; ( 0. <= a1 . n & 0. <= (M * F1) . n ) by A26, A29, A33, A30, A35; then 0. <= (a1 . n) * ((M * F1) . n) ; hence contradiction by A27, A35, A36; ::_thesis: verum end; now__::_thesis:_(_(_ex_i,_j_being_Nat_st_ (_i_in_dom_F1_&_j_in_dom_F2_&_2_<=_i_&_2_<=_j_&_M_._((F1_._i)_/\_(F2_._j))_=_+infty_)_&_s1_=_s2_)_or_(_(_for_i,_j_being_Nat_st_i_in_dom_F1_&_j_in_dom_F2_&_2_<=_i_&_2_<=_j_holds_ M_._((F1_._i)_/\_(F2_._j))_<>_+infty_)_&_s1_=_s2_)_) percases ( ex i, j being Nat st ( i in dom F1 & j in dom F2 & 2 <= i & 2 <= j & M . ((F1 . i) /\ (F2 . j)) = +infty ) or for i, j being Nat st i in dom F1 & j in dom F2 & 2 <= i & 2 <= j holds M . ((F1 . i) /\ (F2 . j)) <> +infty ) ; case ex i, j being Nat st ( i in dom F1 & j in dom F2 & 2 <= i & 2 <= j & M . ((F1 . i) /\ (F2 . j)) = +infty ) ; ::_thesis: s1 = s2 then consider i, j being Nat such that A36: i in dom F1 and A37: j in dom F2 and A38: 2 <= i and A39: 2 <= j and A40: M . ((F1 . i) /\ (F2 . j)) = +infty ; A41: F2 . j in rng F2 by A37, FUNCT_1:3; A42: F1 . i in rng F1 by A36, FUNCT_1:3; then A43: (F1 . i) /\ (F2 . j) in S by A41, MEASURE1:34; (F1 . i) /\ (F2 . j) c= F1 . i by XBOOLE_1:17; then M . (F1 . i) = +infty by A40, A42, A43, MEASURE1:31, XXREAL_0:4; then A44: (M * F1) . i = +infty by A36, FUNCT_1:13; 0. < a1 . i by A25, A29, A36, A38; then +infty = (a1 . i) * ((M * F1) . i) by A44, XXREAL_3:def_5; then x1 . i = +infty by A26, A27, A36; then +infty in rng x1 by A26, A36, FUNCT_1:def_3; then A45: Sum x1 = +infty by A34, Th17; (F1 . i) /\ (F2 . j) c= F2 . j by XBOOLE_1:17; then M . (F2 . j) = +infty by A40, A41, A43, MEASURE1:31, XXREAL_0:4; then A46: (M * F2) . j = +infty by A37, FUNCT_1:13; 0. < a2 . j by A12, A16, A37, A39; then +infty = (a2 . j) * ((M * F2) . j) by A46, XXREAL_3:def_5; then x2 . j = +infty by A13, A14, A37; then +infty in rng x2 by A13, A37, FUNCT_1:def_3; hence s1 = s2 by A28, A15, A21, A45, Th17; ::_thesis: verum end; caseA47: for i, j being Nat st i in dom F1 & j in dom F2 & 2 <= i & 2 <= j holds M . ((F1 . i) /\ (F2 . j)) <> +infty ; ::_thesis: s1 = s2 set m = len x2; set n = len x1; ex a being Function of [:(Seg (len x1)),(Seg (len x2)):],REAL st for i, j being Nat st i in Seg (len x1) & j in Seg (len x2) holds a . (i,j) = (a1 . i) * (M . ((F1 . i) /\ (F2 . j))) proof deffunc H1( set , set ) -> Element of ExtREAL = (a1 . \$1) * (M . ((F1 . \$1) /\ (F2 . \$2))); A48: for x, y being set st x in Seg (len x1) & y in Seg (len x2) holds H1(x,y) in REAL proof let x, y be set ; ::_thesis: ( x in Seg (len x1) & y in Seg (len x2) implies H1(x,y) in REAL ) assume that A49: x in Seg (len x1) and A50: y in Seg (len x2) ; ::_thesis: H1(x,y) in REAL x in { k where k is Element of NAT : ( 1 <= k & k <= len x1 ) } by A49, FINSEQ_1:def_1; then consider kx being Element of NAT such that A51: x = kx and A52: 1 <= kx and kx <= len x1 ; y in { k where k is Element of NAT : ( 1 <= k & k <= len x2 ) } by A50, FINSEQ_1:def_1; then consider ky being Element of NAT such that A53: y = ky and A54: 1 <= ky and ky <= len x2 ; A55: ky in dom F2 by A13, A50, A53, FINSEQ_1:def_3; then A56: F2 . ky in rng F2 by FUNCT_1:3; A57: kx in dom F1 by A26, A49, A51, FINSEQ_1:def_3; then F1 . kx in rng F1 by FUNCT_1:3; then A58: (F1 . kx) /\ (F2 . ky) in S by A56, MEASURE1:34; now__::_thesis:_(_(_(_not_2_<=_kx_or_not_2_<=_ky_)_&_H1(kx,ky)_in_REAL_)_or_(_2_<=_kx_&_2_<=_ky_&_H1(kx,ky)_in_REAL_)_) percases ( not 2 <= kx or not 2 <= ky or ( 2 <= kx & 2 <= ky ) ) ; caseA59: ( not 2 <= kx or not 2 <= ky ) ; ::_thesis: H1(kx,ky) in REAL now__::_thesis:_(_(_kx_<_2_&_H1(kx,ky)_in_REAL_)_or_(_ky_<_2_&_H1(kx,ky)_in_REAL_)_) percases ( kx < 2 or ky < 2 ) by A59; caseA60: kx < 2 ; ::_thesis: H1(kx,ky) in REAL then kx <= 1 + 1 ; then kx <= 1 by A60, NAT_1:8; then H1(kx,ky) = 0. * (M . ((F1 . kx) /\ (F2 . ky))) by A24, A52, XXREAL_0:1 .= 0 ; hence H1(kx,ky) in REAL ; ::_thesis: verum end; caseA61: ky < 2 ; ::_thesis: H1(kx,ky) in REAL then ky <= 1 + 1 ; then A62: ky <= 1 by A61, NAT_1:8; now__::_thesis:_(_(_(F1_._kx)_/\_(F2_._ky)_=_{}_&_H1(kx,ky)_=_0_)_or_(_(F1_._kx)_/\_(F2_._ky)_<>_{}_&_H1(kx,ky)_=_0_)_) percases ( (F1 . kx) /\ (F2 . ky) = {} or (F1 . kx) /\ (F2 . ky) <> {} ) ; case (F1 . kx) /\ (F2 . ky) = {} ; ::_thesis: H1(kx,ky) = 0 hence H1(kx,ky) = (a1 . kx) * 0. by VALUED_0:def_19 .= 0 ; ::_thesis: verum end; case (F1 . kx) /\ (F2 . ky) <> {} ; ::_thesis: H1(kx,ky) = 0 then consider x being set such that A63: x in (F1 . kx) /\ (F2 . ky) by XBOOLE_0:def_1; A64: x in F2 . ky by A63, XBOOLE_0:def_4; x in F1 . kx by A63, XBOOLE_0:def_4; then a1 . kx = f . x by A23, A57, Def1 .= a2 . ky by A10, A55, A64, Def1 .= 0. by A11, A54, A62, XXREAL_0:1 ; hence H1(kx,ky) = 0 ; ::_thesis: verum end; end; end; hence H1(kx,ky) in REAL ; ::_thesis: verum end; end; end; hence H1(kx,ky) in REAL ; ::_thesis: verum end; caseA65: ( 2 <= kx & 2 <= ky ) ; ::_thesis: H1(kx,ky) in REAL A66: 0. <= a1 . kx by A29, A30, A57; a1 . kx <> +infty by A25, A29, A57, A65; then reconsider r2 = a1 . kx as Real by A66, XXREAL_0:14; 0. <= M . ((F1 . kx) /\ (F2 . ky)) by A58, SUPINF_2:39; then reconsider r3 = M . ((F1 . kx) /\ (F2 . ky)) as Real by A47, A57, A55, A65, XXREAL_0:14; (a1 . kx) * (M . ((F1 . kx) /\ (F2 . ky))) = r2 * r3 by EXTREAL1:1; hence H1(kx,ky) in REAL ; ::_thesis: verum end; end; end; hence H1(x,y) in REAL by A51, A53; ::_thesis: verum end; consider f being Function of [:(Seg (len x1)),(Seg (len x2)):],REAL such that A67: for x, y being set st x in Seg (len x1) & y in Seg (len x2) holds f . (x,y) = H1(x,y) from BINOP_1:sch_2(A48); take f ; ::_thesis: for i, j being Nat st i in Seg (len x1) & j in Seg (len x2) holds f . (i,j) = (a1 . i) * (M . ((F1 . i) /\ (F2 . j))) thus for i, j being Nat st i in Seg (len x1) & j in Seg (len x2) holds f . (i,j) = (a1 . i) * (M . ((F1 . i) /\ (F2 . j))) by A67; ::_thesis: verum end; then consider a being Function of [:(Seg (len x1)),(Seg (len x2)):],REAL such that A68: for i, j being Nat st i in Seg (len x1) & j in Seg (len x2) holds a . (i,j) = (a1 . i) * (M . ((F1 . i) /\ (F2 . j))) ; ex p being FinSequence of REAL st ( dom p = Seg (len x1) & ( for i being Nat st i in dom p holds ex r being FinSequence of REAL st ( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) ) ) proof defpred S1[ Nat, set ] means ex r being FinSequence of REAL st ( dom r = Seg (len x2) & \$2 = Sum r & ( for j being Nat st j in dom r holds r . j = a . [\$1,j] ) ); A69: for k being Nat st k in Seg (len x1) holds ex x being set st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len x1) implies ex x being set st S1[k,x] ) assume k in Seg (len x1) ; ::_thesis: ex x being set st S1[k,x] deffunc H1( set ) -> Element of REAL = a . [k,\$1]; consider r being FinSequence such that A70: len r = len x2 and A71: for i being Nat st i in dom r holds r . i = H1(i) from FINSEQ_1:sch_2(); A72: dom r = Seg (len x2) by A70, FINSEQ_1:def_3; for i being Nat st i in dom r holds r . i in REAL proof let i be Nat; ::_thesis: ( i in dom r implies r . i in REAL ) A73: a . [k,i] in REAL ; assume i in dom r ; ::_thesis: r . i in REAL hence r . i in REAL by A71, A73; ::_thesis: verum end; then reconsider r = r as FinSequence of REAL by FINSEQ_2:12; take x = Sum r; ::_thesis: S1[k,x] thus S1[k,x] by A71, A72; ::_thesis: verum end; consider p being FinSequence such that A74: ( dom p = Seg (len x1) & ( for k being Nat st k in Seg (len x1) holds S1[k,p . k] ) ) from FINSEQ_1:sch_1(A69); for i being Nat st i in dom p holds p . i in REAL proof let i be Nat; ::_thesis: ( i in dom p implies p . i in REAL ) assume i in dom p ; ::_thesis: p . i in REAL then ex r being FinSequence of REAL st ( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) by A74; hence p . i in REAL ; ::_thesis: verum end; then reconsider p = p as FinSequence of REAL by FINSEQ_2:12; take p ; ::_thesis: ( dom p = Seg (len x1) & ( for i being Nat st i in dom p holds ex r being FinSequence of REAL st ( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) ) ) thus ( dom p = Seg (len x1) & ( for i being Nat st i in dom p holds ex r being FinSequence of REAL st ( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) ) ) by A74; ::_thesis: verum end; then consider p being FinSequence of REAL such that A75: dom p = Seg (len x1) and A76: for i being Nat st i in dom p holds ex r being FinSequence of REAL st ( dom r = Seg (len x2) & p . i = Sum r & ( for j being Nat st j in dom r holds r . j = a . [i,j] ) ) ; A77: dom p = dom x1 by A75, FINSEQ_1:def_3; for k being Nat st k in dom p holds p . k = x1 . k proof let k be Nat; ::_thesis: ( k in dom p implies p . k = x1 . k ) assume A78: k in dom p ; ::_thesis: p . k = x1 . k then consider r being FinSequence of REAL such that A79: dom r = Seg (len x2) and A80: p . k = Sum r and A81: for j being Nat st j in dom r holds r . j = a . [k,j] by A76; ex F11 being Finite_Sep_Sequence of S st ( union (rng F11) = F1 . k & dom F11 = dom r & ( for j being Nat st j in dom r holds F11 . j = (F1 . k) /\ (F2 . j) ) ) proof deffunc H1( set ) -> set = (F1 . k) /\ (F2 . \$1); consider F being FinSequence such that A82: len F = len x2 and A83: for i being Nat st i in dom F holds F . i = H1(i) from FINSEQ_1:sch_2(); A84: dom F = Seg (len x2) by A82, FINSEQ_1:def_3; A85: for i being Nat st i in dom F holds F . i in S proof let i be Nat; ::_thesis: ( i in dom F implies F . i in S ) assume A86: i in dom F ; ::_thesis: F . i in S then i in Seg (len x2) by A82, FINSEQ_1:def_3; then i in dom F2 by A13, FINSEQ_1:def_3; then A87: F2 . i in rng F2 by FUNCT_1:3; F1 . k in rng F1 by A26, A77, A78, FUNCT_1:3; then (F1 . k) /\ (F2 . i) in S by A87, MEASURE1:34; hence F . i in S by A83, A86; ::_thesis: verum end; A88: dom F = Seg (len x2) by A82, FINSEQ_1:def_3; reconsider F = F as FinSequence of S by A85, FINSEQ_2:12; A89: dom F = dom F2 by A13, A88, FINSEQ_1:def_3; then reconsider F = F as Finite_Sep_Sequence of S by A83, Th5; take F ; ::_thesis: ( union (rng F) = F1 . k & dom F = dom r & ( for j being Nat st j in dom r holds F . j = (F1 . k) /\ (F2 . j) ) ) union (rng F) = (F1 . k) /\ (union (rng F2)) by A83, A89, Th6 .= (F1 . k) /\ (dom f) by A10, Def1 .= (F1 . k) /\ (union (rng F1)) by A23, Def1 .= F1 . k by A26, A77, A78, Th7 ; hence ( union (rng F) = F1 . k & dom F = dom r & ( for j being Nat st j in dom r holds F . j = (F1 . k) /\ (F2 . j) ) ) by A79, A83, A84; ::_thesis: verum end; then consider F11 being Finite_Sep_Sequence of S such that A90: union (rng F11) = F1 . k and A91: dom F11 = dom r and A92: for j being Nat st j in dom r holds F11 . j = (F1 . k) /\ (F2 . j) ; A93: Sum (M * F11) = M . (F1 . k) by A90, Th9; k in Seg (len a1) by A26, A29, A77, A78, FINSEQ_1:def_3; then A94: 1 <= k by FINSEQ_1:1; ( a1 . k <> -infty & a1 . k <> +infty ) proof percases ( k = 1 or k <> 1 ) ; suppose k = 1 ; ::_thesis: ( a1 . k <> -infty & a1 . k <> +infty ) hence ( a1 . k <> -infty & a1 . k <> +infty ) by A24; ::_thesis: verum end; suppose k <> 1 ; ::_thesis: ( a1 . k <> -infty & a1 . k <> +infty ) then 1 < k by A94, XXREAL_0:1; then 1 + 1 <= k by NAT_1:13; hence ( a1 . k <> -infty & a1 . k <> +infty ) by A25, A26, A29, A77, A78; ::_thesis: verum end; end; end; then A95: a1 . k is Element of REAL by XXREAL_0:14; reconsider rr = r as FinSequence of ExtREAL by Th11; A96: for j being Nat st j in dom r holds r . j = (a1 . k) * (M . ((F1 . k) /\ (F2 . j))) proof let j be Nat; ::_thesis: ( j in dom r implies r . j = (a1 . k) * (M . ((F1 . k) /\ (F2 . j))) ) assume A97: j in dom r ; ::_thesis: r . j = (a1 . k) * (M . ((F1 . k) /\ (F2 . j))) hence r . j = a . (k,j) by A81 .= (a1 . k) * (M . ((F1 . k) /\ (F2 . j))) by A68, A75, A78, A79, A97 ; ::_thesis: verum end; A98: for j being Nat st j in dom rr holds rr . j = (a1 . k) * ((M * F11) . j) proof let j be Nat; ::_thesis: ( j in dom rr implies rr . j = (a1 . k) * ((M * F11) . j) ) assume A99: j in dom rr ; ::_thesis: rr . j = (a1 . k) * ((M * F11) . j) hence rr . j = (a1 . k) * (M . ((F1 . k) /\ (F2 . j))) by A96 .= (a1 . k) * (M . (F11 . j)) by A92, A99 .= (a1 . k) * ((M * F11) . j) by A91, A99, FUNCT_1:13 ; ::_thesis: verum end; dom rr = dom (M * F11) by A91, Th8; then Sum rr = (a1 . k) * (Sum (M * F11)) by A98, A95, Th10; then Sum r = (a1 . k) * (M . (F1 . k)) by A93, Th2 .= (a1 . k) * ((M * F1) . k) by A26, A77, A78, FUNCT_1:13 ; hence p . k = x1 . k by A27, A77, A78, A80; ::_thesis: verum end; then A100: Sum p = Sum x1 by A77, Th2, FINSEQ_1:13; ex q being FinSequence of REAL st ( dom q = Seg (len x2) & ( for j being Nat st j in dom q holds ex s being FinSequence of REAL st ( dom s = Seg (len x1) & q . j = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,j] ) ) ) ) proof defpred S1[ Nat, set ] means ex s being FinSequence of REAL st ( dom s = Seg (len x1) & \$2 = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,\$1] ) ); A101: for k being Nat st k in Seg (len x2) holds ex x being set st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len x2) implies ex x being set st S1[k,x] ) assume k in Seg (len x2) ; ::_thesis: ex x being set st S1[k,x] deffunc H1( set ) -> Element of REAL = a . [\$1,k]; consider s being FinSequence such that A102: len s = len x1 and A103: for i being Nat st i in dom s holds s . i = H1(i) from FINSEQ_1:sch_2(); A104: dom s = Seg (len x1) by A102, FINSEQ_1:def_3; for i being Nat st i in dom s holds s . i in REAL proof let i be Nat; ::_thesis: ( i in dom s implies s . i in REAL ) A105: a . [i,k] in REAL ; assume i in dom s ; ::_thesis: s . i in REAL hence s . i in REAL by A103, A105; ::_thesis: verum end; then reconsider s = s as FinSequence of REAL by FINSEQ_2:12; take x = Sum s; ::_thesis: S1[k,x] thus S1[k,x] by A103, A104; ::_thesis: verum end; consider p being FinSequence such that A106: ( dom p = Seg (len x2) & ( for k being Nat st k in Seg (len x2) holds S1[k,p . k] ) ) from FINSEQ_1:sch_1(A101); for i being Nat st i in dom p holds p . i in REAL proof let i be Nat; ::_thesis: ( i in dom p implies p . i in REAL ) assume i in dom p ; ::_thesis: p . i in REAL then ex s being FinSequence of REAL st ( dom s = Seg (len x1) & p . i = Sum s & ( for j being Nat st j in dom s holds s . j = a . [j,i] ) ) by A106; hence p . i in REAL ; ::_thesis: verum end; then reconsider p = p as FinSequence of REAL by FINSEQ_2:12; take p ; ::_thesis: ( dom p = Seg (len x2) & ( for j being Nat st j in dom p holds ex s being FinSequence of REAL st ( dom s = Seg (len x1) & p . j = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,j] ) ) ) ) thus ( dom p = Seg (len x2) & ( for j being Nat st j in dom p holds ex s being FinSequence of REAL st ( dom s = Seg (len x1) & p . j = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,j] ) ) ) ) by A106; ::_thesis: verum end; then consider q being FinSequence of REAL such that A107: dom q = Seg (len x2) and A108: for j being Nat st j in dom q holds ex s being FinSequence of REAL st ( dom s = Seg (len x1) & q . j = Sum s & ( for i being Nat st i in dom s holds s . i = a . [i,j] ) ) ; A109: dom q = dom x2 by A107, FINSEQ_1:def_3; A110: for k being Nat st k in dom q holds q . k = x2 . k proof let k be Nat; ::_thesis: ( k in dom q implies q . k = x2 . k ) assume A111: k in dom q ; ::_thesis: q . k = x2 . k then consider s being FinSequence of REAL such that A112: dom s = Seg (len x1) and A113: q . k = Sum s and A114: for i being Nat st i in dom s holds s . i = a . [i,k] by A108; reconsider ss = s as FinSequence of ExtREAL by Th11; ex F21 being Finite_Sep_Sequence of S st ( union (rng F21) = F2 . k & dom F21 = dom s & ( for j being Nat st j in dom s holds F21 . j = (F1 . j) /\ (F2 . k) ) ) proof deffunc H1( set ) -> set = (F2 . k) /\ (F1 . \$1); consider F being FinSequence such that A115: len F = len x1 and A116: for i being Nat st i in dom F holds F . i = H1(i) from FINSEQ_1:sch_2(); A117: dom F = Seg (len x1) by A115, FINSEQ_1:def_3; A118: for i being Nat st i in dom F holds F . i in S proof let i be Nat; ::_thesis: ( i in dom F implies F . i in S ) assume A119: i in dom F ; ::_thesis: F . i in S then i in Seg (len x1) by A115, FINSEQ_1:def_3; then i in dom F1 by A26, FINSEQ_1:def_3; then A120: F1 . i in rng F1 by FUNCT_1:3; F2 . k in rng F2 by A13, A109, A111, FUNCT_1:3; then (F1 . i) /\ (F2 . k) in S by A120, MEASURE1:34; hence F . i in S by A116, A119; ::_thesis: verum end; A121: dom F = Seg (len x1) by A115, FINSEQ_1:def_3; reconsider F = F as FinSequence of S by A118, FINSEQ_2:12; A122: dom F = dom F1 by A26, A121, FINSEQ_1:def_3; then reconsider F = F as Finite_Sep_Sequence of S by A116, Th5; take F ; ::_thesis: ( union (rng F) = F2 . k & dom F = dom s & ( for j being Nat st j in dom s holds F . j = (F1 . j) /\ (F2 . k) ) ) union (rng F) = (F2 . k) /\ (union (rng F1)) by A116, A122, Th6 .= (F2 . k) /\ (dom f) by A23, Def1 .= (F2 . k) /\ (union (rng F2)) by A10, Def1 .= F2 . k by A13, A109, A111, Th7 ; hence ( union (rng F) = F2 . k & dom F = dom s & ( for j being Nat st j in dom s holds F . j = (F1 . j) /\ (F2 . k) ) ) by A112, A116, A117; ::_thesis: verum end; then consider F21 being Finite_Sep_Sequence of S such that A123: union (rng F21) = F2 . k and A124: dom F21 = dom s and A125: for i being Nat st i in dom s holds F21 . i = (F1 . i) /\ (F2 . k) ; A126: Sum (M * F21) = M . (F2 . k) by A123, Th9; A127: for i being Nat st i in dom s holds s . i = (a1 . i) * (M . ((F1 . i) /\ (F2 . k))) proof let i be Nat; ::_thesis: ( i in dom s implies s . i = (a1 . i) * (M . ((F1 . i) /\ (F2 . k))) ) assume A128: i in dom s ; ::_thesis: s . i = (a1 . i) * (M . ((F1 . i) /\ (F2 . k))) hence s . i = a . (i,k) by A114 .= (a1 . i) * (M . ((F1 . i) /\ (F2 . k))) by A68, A107, A111, A112, A128 ; ::_thesis: verum end; A129: for i being Nat st i in dom s holds s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) proof let i be Nat; ::_thesis: ( i in dom s implies s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) ) assume A130: i in dom s ; ::_thesis: s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) now__::_thesis:_(_(_(F1_._i)_/\_(F2_._k)_=_{}_&_s_._i_=_(a2_._k)_*_(M_._((F1_._i)_/\_(F2_._k)))_)_or_(_(F1_._i)_/\_(F2_._k)_<>_{}_&_s_._i_=_(a2_._k)_*_(M_._((F1_._i)_/\_(F2_._k)))_)_) percases ( (F1 . i) /\ (F2 . k) = {} or (F1 . i) /\ (F2 . k) <> {} ) ; caseA131: (F1 . i) /\ (F2 . k) = {} ; ::_thesis: s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) then M . ((F1 . i) /\ (F2 . k)) = 0. by VALUED_0:def_19; hence s . i = (a1 . i) * 0. by A127, A130 .= 0. .= (a2 . k) * 0. .= (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) by A131, VALUED_0:def_19 ; ::_thesis: verum end; case (F1 . i) /\ (F2 . k) <> {} ; ::_thesis: s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) then consider x being set such that A132: x in (F1 . i) /\ (F2 . k) by XBOOLE_0:def_1; A133: x in F2 . k by A132, XBOOLE_0:def_4; A134: dom p = dom x1 by A75, FINSEQ_1:def_3; x in F1 . i by A132, XBOOLE_0:def_4; then a1 . i = f . x by A23, A26, A75, A112, A130, A134, Def1 .= a2 . k by A10, A13, A109, A111, A133, Def1 ; hence s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) by A127, A130; ::_thesis: verum end; end; end; hence s . i = (a2 . k) * (M . ((F1 . i) /\ (F2 . k))) ; ::_thesis: verum end; A135: for j being Nat st j in dom ss holds ss . j = (a2 . k) * ((M * F21) . j) proof let j be Nat; ::_thesis: ( j in dom ss implies ss . j = (a2 . k) * ((M * F21) . j) ) assume A136: j in dom ss ; ::_thesis: ss . j = (a2 . k) * ((M * F21) . j) hence ss . j = (a2 . k) * (M . ((F1 . j) /\ (F2 . k))) by A129 .= (a2 . k) * (M . (F21 . j)) by A125, A136 .= (a2 . k) * ((M * F21) . j) by A124, A136, FUNCT_1:13 ; ::_thesis: verum end; k in Seg (len a2) by A13, A16, A109, A111, FINSEQ_1:def_3; then A137: 1 <= k by FINSEQ_1:1; ( a2 . k <> -infty & a2 . k <> +infty ) proof percases ( k = 1 or k <> 1 ) ; suppose k = 1 ; ::_thesis: ( a2 . k <> -infty & a2 . k <> +infty ) hence ( a2 . k <> -infty & a2 . k <> +infty ) by A11; ::_thesis: verum end; suppose k <> 1 ; ::_thesis: ( a2 . k <> -infty & a2 . k <> +infty ) then 1 < k by A137, XXREAL_0:1; then 1 + 1 <= k by NAT_1:13; hence ( a2 . k <> -infty & a2 . k <> +infty ) by A12, A13, A16, A109, A111; ::_thesis: verum end; end; end; then A138: a2 . k is Element of REAL by XXREAL_0:14; dom ss = dom (M * F21) by A124, Th8; then Sum ss = (a2 . k) * (Sum (M * F21)) by A135, A138, Th10; then Sum s = (a2 . k) * (M . (F2 . k)) by A126, Th2 .= (a2 . k) * ((M * F2) . k) by A13, A109, A111, FUNCT_1:13 ; hence q . k = x2 . k by A14, A109, A111, A113; ::_thesis: verum end; Sum p = Sum q by A75, A76, A107, A108, Th1; hence s1 = s2 by A28, A15, A100, A109, A110, Th2, FINSEQ_1:13; ::_thesis: verum end; end; end; hence s1 = s2 ; ::_thesis: verum end; end; end; :: deftheorem defines integral MESFUNC3:def_2_:_ for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds 0. <= f . x ) holds for b5 being Element of ExtREAL holds ( b5 = integral (X,S,M,f) iff ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds ( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & b5 = Sum x ) ); begin theorem :: MESFUNC3:18 for a being FinSequence of ExtREAL for p, N being Element of ExtREAL st N = len a & ( for n being Nat st n in dom a holds a . n = p ) holds Sum a = N * p by Lm1;