:: MESFUNC4 semantic presentation begin theorem Th1: :: MESFUNC4:1 for F, G, H being FinSequence of ExtREAL st ( for i being Nat st i in dom F holds 0. <= F . i ) & ( for i being Nat st i in dom G holds 0. <= G . i ) & dom F = dom G & H = F + G holds Sum H = (Sum F) + (Sum G) proof let F, G, H be FinSequence of ExtREAL ; ::_thesis: ( ( for i being Nat st i in dom F holds 0. <= F . i ) & ( for i being Nat st i in dom G holds 0. <= G . i ) & dom F = dom G & H = F + G implies Sum H = (Sum F) + (Sum G) ) assume that A1: for i being Nat st i in dom F holds 0. <= F . i and A2: for i being Nat st i in dom G holds 0. <= G . i and A3: dom F = dom G and A4: H = F + G ; ::_thesis: Sum H = (Sum F) + (Sum G) for y being set st y in rng F holds not y in {-infty} proof let y be set ; ::_thesis: ( y in rng F implies not y in {-infty} ) assume y in rng F ; ::_thesis: not y in {-infty} then consider x being set such that A5: x in dom F and A6: y = F . x by FUNCT_1:def_3; reconsider x = x as Element of NAT by A5; 0. <= F . x by A1, A5; hence not y in {-infty} by A6, TARSKI:def_1; ::_thesis: verum end; then rng F misses {-infty} by XBOOLE_0:3; then A7: F " {-infty} = {} by RELAT_1:138; for y being set st y in rng G holds not y in {-infty} proof let y be set ; ::_thesis: ( y in rng G implies not y in {-infty} ) assume y in rng G ; ::_thesis: not y in {-infty} then consider x being set such that A8: x in dom G and A9: y = G . x by FUNCT_1:def_3; reconsider x = x as Element of NAT by A8; 0. <= G . x by A2, A8; hence not y in {-infty} by A9, TARSKI:def_1; ::_thesis: verum end; then rng G misses {-infty} by XBOOLE_0:3; then A10: G " {-infty} = {} by RELAT_1:138; A11: dom H = ((dom F) /\ (dom G)) \ (((F " {-infty}) /\ (G " {+infty})) \/ ((F " {+infty}) /\ (G " {-infty}))) by A4, MESFUNC1:def_3 .= dom F by A3, A7, A10 ; then A12: len H = len F by FINSEQ_3:29; consider h being Function of NAT,ExtREAL such that A13: Sum H = h . (len H) and A14: h . 0 = 0. and A15: for i being Element of NAT st i < len H holds h . (i + 1) = (h . i) + (H . (i + 1)) by EXTREAL1:def_2; consider f being Function of NAT,ExtREAL such that A16: Sum F = f . (len F) and A17: f . 0 = 0. and A18: for i being Element of NAT st i < len F holds f . (i + 1) = (f . i) + (F . (i + 1)) by EXTREAL1:def_2; consider g being Function of NAT,ExtREAL such that A19: Sum G = g . (len G) and A20: g . 0 = 0. and A21: for i being Element of NAT st i < len G holds g . (i + 1) = (g . i) + (G . (i + 1)) by EXTREAL1:def_2; defpred S1[ Nat] means ( $1 <= len H implies h . $1 = (f . $1) + (g . $1) ); A22: len H = len G by A3, A11, FINSEQ_3:29; A23: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A24: S1[k] ; ::_thesis: S1[k + 1] assume A25: k + 1 <= len H ; ::_thesis: h . (k + 1) = (f . (k + 1)) + (g . (k + 1)) reconsider k = k as Element of NAT by ORDINAL1:def_12; A26: k < len H by A25, NAT_1:13; then A27: ( f . (k + 1) = (f . k) + (F . (k + 1)) & g . (k + 1) = (g . k) + (G . (k + 1)) ) by A18, A21, A12, A22; 1 <= k + 1 by NAT_1:11; then A28: k + 1 in dom H by A25, FINSEQ_3:25; A29: ( f . k <> -infty & g . k <> -infty & F . (k + 1) <> -infty & G . (k + 1) <> -infty ) proof defpred S2[ Nat] means ( $1 <= len H implies g . $1 <> -infty ); defpred S3[ Nat] means ( $1 <= len H implies f . $1 <> -infty ); A30: for m being Nat st S3[m] holds S3[m + 1] proof let m be Nat; ::_thesis: ( S3[m] implies S3[m + 1] ) assume A31: S3[m] ; ::_thesis: S3[m + 1] assume A32: m + 1 <= len H ; ::_thesis: f . (m + 1) <> -infty reconsider m = m as Element of NAT by ORDINAL1:def_12; 1 <= m + 1 by NAT_1:11; then m + 1 in dom H by A32, FINSEQ_3:25; then A33: 0. <= F . (m + 1) by A1, A11; m < len H by A32, NAT_1:13; then f . (m + 1) = (f . m) + (F . (m + 1)) by A18, A12; hence f . (m + 1) <> -infty by A31, A32, A33, NAT_1:13, XXREAL_3:17; ::_thesis: verum end; A34: S3[ 0 ] by A17; for i being Nat holds S3[i] from NAT_1:sch_2(A34, A30); hence f . k <> -infty by A26; ::_thesis: ( g . k <> -infty & F . (k + 1) <> -infty & G . (k + 1) <> -infty ) A35: for m being Nat st S2[m] holds S2[m + 1] proof let m be Nat; ::_thesis: ( S2[m] implies S2[m + 1] ) assume A36: S2[m] ; ::_thesis: S2[m + 1] assume A37: m + 1 <= len H ; ::_thesis: g . (m + 1) <> -infty reconsider m = m as Element of NAT by ORDINAL1:def_12; 1 <= m + 1 by NAT_1:11; then m + 1 in dom H by A37, FINSEQ_3:25; then A38: 0. <= G . (m + 1) by A2, A3, A11; m < len H by A37, NAT_1:13; then g . (m + 1) = (g . m) + (G . (m + 1)) by A21, A22; hence g . (m + 1) <> -infty by A36, A37, A38, NAT_1:13, XXREAL_3:17; ::_thesis: verum end; A39: S2[ 0 ] by A20; for i being Nat holds S2[i] from NAT_1:sch_2(A39, A35); hence g . k <> -infty by A26; ::_thesis: ( F . (k + 1) <> -infty & G . (k + 1) <> -infty ) thus F . (k + 1) <> -infty by A1, A11, A28; ::_thesis: G . (k + 1) <> -infty thus G . (k + 1) <> -infty by A2, A3, A11, A28; ::_thesis: verum end; then A40: (f . k) + (F . (k + 1)) <> -infty by XXREAL_3:17; A41: h . (k + 1) = ((f . k) + (g . k)) + (H . (k + 1)) by A15, A24, A26 .= ((f . k) + (g . k)) + ((F . (k + 1)) + (G . (k + 1))) by A4, A28, MESFUNC1:def_3 ; (f . k) + (g . k) <> -infty by A29, XXREAL_3:17; then h . (k + 1) = (((f . k) + (g . k)) + (F . (k + 1))) + (G . (k + 1)) by A41, A29, XXREAL_3:29 .= (((f . k) + (F . (k + 1))) + (g . k)) + (G . (k + 1)) by A29, XXREAL_3:29 .= (f . (k + 1)) + (g . (k + 1)) by A27, A29, A40, XXREAL_3:29 ; hence h . (k + 1) = (f . (k + 1)) + (g . (k + 1)) ; ::_thesis: verum end; A42: S1[ 0 ] by A17, A20, A14; for i being Nat holds S1[i] from NAT_1:sch_2(A42, A23); hence Sum H = (Sum F) + (Sum G) by A16, A19, A13, A12, A22; ::_thesis: verum end; theorem Th2: :: MESFUNC4:2 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for n being Nat for f being PartFunc of X,ExtREAL for F being Finite_Sep_Sequence of S for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds x . i = (a . i) * ((M * F) . i) ) & len F = n holds integral (X,S,M,f) = Sum x proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for n being Nat for f being PartFunc of X,ExtREAL for F being Finite_Sep_Sequence of S for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds x . i = (a . i) * ((M * F) . i) ) & len F = n holds integral (X,S,M,f) = Sum x let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for n being Nat for f being PartFunc of X,ExtREAL for F being Finite_Sep_Sequence of S for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds x . i = (a . i) * ((M * F) . i) ) & len F = n holds integral (X,S,M,f) = Sum x let M be sigma_Measure of S; ::_thesis: for n being Nat for f being PartFunc of X,ExtREAL for F being Finite_Sep_Sequence of S for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds x . i = (a . i) * ((M * F) . i) ) & len F = n holds integral (X,S,M,f) = Sum x defpred S1[ Nat] means for f being PartFunc of X,ExtREAL for F being Finite_Sep_Sequence of S for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds x . i = (a . i) * ((M * F) . i) ) & len F = $1 holds integral (X,S,M,f) = Sum x; 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 PartFunc of X,ExtREAL; ::_thesis: for F being Finite_Sep_Sequence of S for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds x . i = (a . i) * ((M * F) . i) ) & len F = n + 1 holds integral (X,S,M,f) = Sum x let F be Finite_Sep_Sequence of S; ::_thesis: for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds x . i = (a . i) * ((M * F) . i) ) & len F = n + 1 holds integral (X,S,M,f) = Sum x let a, x be FinSequence of ExtREAL ; ::_thesis: ( f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds x . i = (a . i) * ((M * F) . i) ) & len F = n + 1 implies integral (X,S,M,f) = Sum x ) assume that A3: f is_simple_func_in S and A4: dom f <> {} and A5: for x being set st x in dom f holds 0. <= f . x and A6: F,a are_Re-presentation_of f and A7: dom x = dom F and A8: for i being Nat st i in dom x holds x . i = (a . i) * ((M * F) . i) and A9: len F = n + 1 ; ::_thesis: integral (X,S,M,f) = Sum x A10: f is V63() by A3, MESFUNC2:def_4; reconsider n = n as Element of NAT by ORDINAL1:def_12; set F1 = F | (Seg n); set f1 = f | (union (rng (F | (Seg n)))); reconsider F1 = F | (Seg n) as Finite_Sep_Sequence of S by MESFUNC2:33; A11: dom (f | (union (rng (F | (Seg n))))) = (dom f) /\ (union (rng F1)) by RELAT_1:61 .= (union (rng F)) /\ (union (rng F1)) by A6, MESFUNC3:def_1 ; A12: for x being set st x in dom (f | (union (rng (F | (Seg n))))) holds 0. <= (f | (union (rng (F | (Seg n))))) . x proof let x be set ; ::_thesis: ( x in dom (f | (union (rng (F | (Seg n))))) implies 0. <= (f | (union (rng (F | (Seg n))))) . x ) assume A13: x in dom (f | (union (rng (F | (Seg n))))) ; ::_thesis: 0. <= (f | (union (rng (F | (Seg n))))) . x then ( dom (f | (union (rng (F | (Seg n))))) c= dom f & (f | (union (rng (F | (Seg n))))) . x = f . x ) by FUNCT_1:47, RELAT_1:60; hence 0. <= (f | (union (rng (F | (Seg n))))) . x by A5, A13; ::_thesis: verum end; set a1 = a | (Seg n); reconsider a1 = a | (Seg n) as FinSequence of ExtREAL by FINSEQ_1:18; set x1 = x | (Seg n); reconsider x1 = x | (Seg n) as FinSequence of ExtREAL by FINSEQ_1:18; A14: dom x1 = (dom F) /\ (Seg n) by A7, RELAT_1:61 .= dom F1 by RELAT_1:61 ; A15: union (rng F1) c= union (rng F) by RELAT_1:70, ZFMISC_1:77; then A16: dom (f | (union (rng (F | (Seg n))))) = union (rng F1) by A11, XBOOLE_1:28; ex F19 being Finite_Sep_Sequence of S st ( dom (f | (union (rng (F | (Seg n))))) = union (rng F19) & ( for n being Nat for x, y being Element of X st n in dom F19 & x in F19 . n & y in F19 . n holds (f | (union (rng (F | (Seg n))))) . x = (f | (union (rng (F | (Seg n))))) . y ) ) proof take F1 ; ::_thesis: ( dom (f | (union (rng (F | (Seg n))))) = union (rng F1) & ( 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 | (union (rng (F | (Seg n))))) . x = (f | (union (rng (F | (Seg n))))) . y ) ) 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 | (union (rng (F | (Seg n))))) . x = (f | (union (rng (F | (Seg n))))) . y proof let n be Nat; ::_thesis: for x, y being Element of X st n in dom F1 & x in F1 . n & y in F1 . n holds (f | (union (rng (F | (Seg n))))) . x = (f | (union (rng (F | (Seg n))))) . y let x, y be Element of X; ::_thesis: ( n in dom F1 & x in F1 . n & y in F1 . n implies (f | (union (rng (F | (Seg n))))) . x = (f | (union (rng (F | (Seg n))))) . y ) assume that A17: n in dom F1 and A18: x in F1 . n and A19: y in F1 . n ; ::_thesis: (f | (union (rng (F | (Seg n))))) . x = (f | (union (rng (F | (Seg n))))) . y F1 . n c= dom (f | (union (rng (F | (Seg n))))) by A16, A17, FUNCT_1:3, ZFMISC_1:74; then A20: ( (f | (union (rng (F | (Seg n))))) . x = f . x & (f | (union (rng (F | (Seg n))))) . y = f . y ) by A18, A19, FUNCT_1:47; A21: dom F1 c= dom F by RELAT_1:60; A22: F1 . n = F . n by A17, FUNCT_1:47; then f . x = a . n by A6, A17, A18, A21, MESFUNC3:def_1; hence (f | (union (rng (F | (Seg n))))) . x = (f | (union (rng (F | (Seg n))))) . y by A6, A17, A19, A20, A22, A21, MESFUNC3:def_1; ::_thesis: verum end; hence ( dom (f | (union (rng (F | (Seg n))))) = union (rng F1) & ( 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 | (union (rng (F | (Seg n))))) . x = (f | (union (rng (F | (Seg n))))) . y ) ) by A11, A15, XBOOLE_1:28; ::_thesis: verum end; then A23: f | (union (rng (F | (Seg n)))) is_simple_func_in S by A10, MESFUNC2:def_4; A24: dom F1 = (dom F) /\ (Seg n) by RELAT_1:61 .= (dom a) /\ (Seg n) by A6, MESFUNC3:def_1 .= dom a1 by RELAT_1:61 ; for n being Nat st n in dom F1 holds for x being set st x in F1 . n holds (f | (union (rng (F | (Seg n))))) . x = a1 . n proof let n be Nat; ::_thesis: ( n in dom F1 implies for x being set st x in F1 . n holds (f | (union (rng (F | (Seg n))))) . x = a1 . n ) assume A25: n in dom F1 ; ::_thesis: for x being set st x in F1 . n holds (f | (union (rng (F | (Seg n))))) . x = a1 . n then A26: ( F1 . n = F . n & a1 . n = a . n ) by A24, FUNCT_1:47; let x be set ; ::_thesis: ( x in F1 . n implies (f | (union (rng (F | (Seg n))))) . x = a1 . n ) assume A27: x in F1 . n ; ::_thesis: (f | (union (rng (F | (Seg n))))) . x = a1 . n F1 . n c= dom (f | (union (rng (F | (Seg n))))) by A16, A25, FUNCT_1:3, ZFMISC_1:74; then ( dom F1 c= dom F & (f | (union (rng (F | (Seg n))))) . x = f . x ) by A27, FUNCT_1:47, RELAT_1:60; hence (f | (union (rng (F | (Seg n))))) . x = a1 . n by A6, A25, A26, A27, MESFUNC3:def_1; ::_thesis: verum end; then A28: F1,a1 are_Re-presentation_of f | (union (rng (F | (Seg n)))) by A16, A24, MESFUNC3:def_1; now__::_thesis:_integral_(X,S,M,f)_=_Sum_x percases ( dom (f | (union (rng (F | (Seg n))))) = {} or dom (f | (union (rng (F | (Seg n))))) <> {} ) ; supposeA29: dom (f | (union (rng (F | (Seg n))))) = {} ; ::_thesis: integral (X,S,M,f) = Sum x 1 <= n + 1 by NAT_1:11; then A30: n + 1 in dom F by A9, FINSEQ_3:25; A31: union (rng F) = (union (rng F1)) \/ (F . (n + 1)) proof thus union (rng F) c= (union (rng F1)) \/ (F . (n + 1)) :: according to XBOOLE_0:def_10 ::_thesis: (union (rng F1)) \/ (F . (n + 1)) c= union (rng F) proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in union (rng F) or v in (union (rng F1)) \/ (F . (n + 1)) ) assume v in union (rng F) ; ::_thesis: v in (union (rng F1)) \/ (F . (n + 1)) then consider A being set such that A32: v in A and A33: A in rng F by TARSKI:def_4; consider i being set such that A34: i in dom F and A35: A = F . i by A33, FUNCT_1:def_3; reconsider i = i as Element of NAT by A34; A36: i in Seg (len F) by A34, FINSEQ_1:def_3; then A37: 1 <= i by FINSEQ_1:1; A38: i <= n + 1 by A9, A36, FINSEQ_1:1; percases ( i = n + 1 or i <> n + 1 ) ; suppose i = n + 1 ; ::_thesis: v in (union (rng F1)) \/ (F . (n + 1)) hence v in (union (rng F1)) \/ (F . (n + 1)) by A32, A35, XBOOLE_0:def_3; ::_thesis: verum end; suppose i <> n + 1 ; ::_thesis: v in (union (rng F1)) \/ (F . (n + 1)) then i < n + 1 by A38, XXREAL_0:1; then i <= n by NAT_1:13; then i in Seg n by A37, FINSEQ_1:1; then i in (dom F) /\ (Seg n) by A34, XBOOLE_0:def_4; then i in dom F1 by RELAT_1:61; then ( F1 . i = A & F1 . i in rng F1 ) by A35, FUNCT_1:3, FUNCT_1:47; then v in union (rng F1) by A32, TARSKI:def_4; hence v in (union (rng F1)) \/ (F . (n + 1)) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in (union (rng F1)) \/ (F . (n + 1)) or v in union (rng F) ) assume A39: v in (union (rng F1)) \/ (F . (n + 1)) ; ::_thesis: v in union (rng F) percases ( v in union (rng F1) or v in F . (n + 1) ) by A39, XBOOLE_0:def_3; suppose v in union (rng F1) ; ::_thesis: v in union (rng F) then consider A being set such that A40: v in A and A41: A in rng F1 by TARSKI:def_4; consider i being set such that A42: i in dom F1 and A43: A = F1 . i by A41, FUNCT_1:def_3; i in (dom F) /\ (Seg n) by A42, RELAT_1:61; then A44: i in dom F by XBOOLE_0:def_4; F . i = A by A42, A43, FUNCT_1:47; then A in rng F by A44, FUNCT_1:3; hence v in union (rng F) by A40, TARSKI:def_4; ::_thesis: verum end; supposeA45: v in F . (n + 1) ; ::_thesis: v in union (rng F) F . (n + 1) in rng F by A30, FUNCT_1:3; hence v in union (rng F) by A45, TARSKI:def_4; ::_thesis: verum end; end; end; A46: Seg (len x) = dom F by A7, FINSEQ_1:def_3 .= Seg (n + 1) by A9, FINSEQ_1:def_3 ; then A47: len x = n + 1 by FINSEQ_1:6; then A48: n < len x by NAT_1:13; consider sumx being Function of NAT,ExtREAL such that A49: Sum x = sumx . (len x) and A50: sumx . 0 = 0. and A51: for m being Element of NAT st m < len x holds sumx . (m + 1) = (sumx . m) + (x . (m + 1)) by EXTREAL1:def_2; defpred S2[ Nat] means ( $1 < len x implies sumx . $1 = 0. ); A52: for m being Nat st m in dom F1 holds F1 . m = {} proof let m be Nat; ::_thesis: ( m in dom F1 implies F1 . m = {} ) assume m in dom F1 ; ::_thesis: F1 . m = {} then F1 . m in rng F1 by FUNCT_1:3; hence F1 . m = {} by A16, A29, XBOOLE_1:3, ZFMISC_1:74; ::_thesis: verum end; A53: for m being Nat st m in dom F1 holds x . m = 0. proof reconsider EMPTY = {} as Element of S by PROB_1:4; let m be Nat; ::_thesis: ( m in dom F1 implies x . m = 0. ) assume A54: m in dom F1 ; ::_thesis: x . m = 0. then F1 . m = {} by A52; then A55: F . m = {} by A54, FUNCT_1:47; m in (dom F) /\ (Seg n) by A54, RELAT_1:61; then A56: m in dom x by A7, XBOOLE_0:def_4; then A57: x . m = (a . m) * ((M * F) . m) by A8; M . EMPTY = 0. by VALUED_0:def_19; then (M * F) . m = 0. by A7, A56, A55, FUNCT_1:13; hence x . m = 0. by A57; ::_thesis: verum end; A58: for m being Nat st S2[m] holds S2[m + 1] proof let m be Nat; ::_thesis: ( S2[m] implies S2[m + 1] ) assume A59: S2[m] ; ::_thesis: S2[m + 1] A60: 1 <= m + 1 by NAT_1:11; assume A61: m + 1 < len x ; ::_thesis: sumx . (m + 1) = 0. then m + 1 <= n by A47, NAT_1:13; then A62: m + 1 in Seg n by A60, FINSEQ_1:1; m + 1 in Seg (len x) by A61, A60, FINSEQ_1:1; then m + 1 in dom F by A7, FINSEQ_1:def_3; then m + 1 in (dom F) /\ (Seg n) by A62, XBOOLE_0:def_4; then A63: m + 1 in dom F1 by RELAT_1:61; A64: m in NAT by ORDINAL1:def_12; m <= m + 1 by NAT_1:11; then m < len x by A61, XXREAL_0:2; then sumx . (m + 1) = 0. + (x . (m + 1)) by A51, A59, A64 .= x . (m + 1) by XXREAL_3:4 ; hence sumx . (m + 1) = 0. by A53, A63; ::_thesis: verum end; A65: S2[ 0 ] by A50; A66: for m being Nat holds S2[m] from NAT_1:sch_2(A65, A58); A67: Sum x = sumx . (n + 1) by A49, A46, FINSEQ_1:6 .= (sumx . n) + (x . (n + 1)) by A51, A48 .= 0. + (x . (n + 1)) by A66, A48 .= x . (n + 1) by XXREAL_3:4 ; now__::_thesis:_(_(_a_._(n_+_1)_<>_0._&_integral_(X,S,M,f)_=_Sum_x_)_or_(_a_._(n_+_1)_=_0._&_integral_(X,S,M,f)_=_Sum_x_)_) percases ( a . (n + 1) <> 0. or a . (n + 1) = 0. ) ; caseA68: a . (n + 1) <> 0. ; ::_thesis: integral (X,S,M,f) = Sum x defpred S3[ Nat, set ] means ( ( $1 = 1 implies $2 = 0. ) & ( $1 = 2 implies $2 = a . (n + 1) ) ); defpred S4[ Nat, set ] means ( ( $1 = 1 implies $2 = union (rng F1) ) & ( $1 = 2 implies $2 = F . (n + 1) ) ); A69: for k being Nat st k in Seg 2 holds ex x being Element of ExtREAL st S3[k,x] proof let k be Nat; ::_thesis: ( k in Seg 2 implies ex x being Element of ExtREAL st S3[k,x] ) assume A70: k in Seg 2 ; ::_thesis: ex x being Element of ExtREAL st S3[k,x] percases ( k = 1 or k = 2 ) by A70, FINSEQ_1:2, TARSKI:def_2; supposeA71: k = 1 ; ::_thesis: ex x being Element of ExtREAL st S3[k,x] set x = 0. ; reconsider x = 0. as Element of ExtREAL ; take x ; ::_thesis: S3[k,x] thus S3[k,x] by A71; ::_thesis: verum end; supposeA72: k = 2 ; ::_thesis: ex x being Element of ExtREAL st S3[k,x] set x = a . (n + 1); reconsider x = a . (n + 1) as Element of ExtREAL ; take x ; ::_thesis: S3[k,x] thus S3[k,x] by A72; ::_thesis: verum end; end; end; consider b being FinSequence of ExtREAL such that A73: ( dom b = Seg 2 & ( for k being Nat st k in Seg 2 holds S3[k,b . k] ) ) from FINSEQ_1:sch_5(A69); A74: for k being Nat st k in Seg 2 holds ex x being Element of S st S4[k,x] proof let k be Nat; ::_thesis: ( k in Seg 2 implies ex x being Element of S st S4[k,x] ) assume A75: k in Seg 2 ; ::_thesis: ex x being Element of S st S4[k,x] percases ( k = 1 or k = 2 ) by A75, FINSEQ_1:2, TARSKI:def_2; supposeA76: k = 1 ; ::_thesis: ex x being Element of S st S4[k,x] set x = union (rng F1); reconsider x = union (rng F1) as Element of S by MESFUNC2:31; take x ; ::_thesis: S4[k,x] thus S4[k,x] by A76; ::_thesis: verum end; supposeA77: k = 2 ; ::_thesis: ex x being Element of S st S4[k,x] set x = F . (n + 1); ( F . (n + 1) in rng F & rng F c= S ) by A30, FINSEQ_1:def_4, FUNCT_1:3; then reconsider x = F . (n + 1) as Element of S ; take x ; ::_thesis: S4[k,x] thus S4[k,x] by A77; ::_thesis: verum end; end; end; consider G being FinSequence of S such that A78: ( dom G = Seg 2 & ( for k being Nat st k in Seg 2 holds S4[k,G . k] ) ) from FINSEQ_1:sch_5(A74); A79: 1 in Seg 2 by FINSEQ_1:2, TARSKI:def_2; then A80: b . 1 = 0. by A73; A81: b . 1 = 0. by A73, A79; 2 in Seg 2 by FINSEQ_1:2, TARSKI:def_2; then A82: b . 2 = a . (n + 1) by A73; A83: 2 in Seg 2 by FINSEQ_1:2, TARSKI:def_2; then A84: G . 2 = F . (n + 1) by A78; A85: 1 in Seg 2 by FINSEQ_1:2, TARSKI:def_2; then A86: G . 1 = union (rng F1) by A78; A87: for u, v being set st u <> v holds G . u misses G . v proof let u, v be set ; ::_thesis: ( u <> v implies G . u misses G . v ) assume A88: u <> v ; ::_thesis: G . u misses G . v percases ( ( u in dom G & v in dom G ) or not u in dom G or not v in dom G ) ; supposeA89: ( u in dom G & v in dom G ) ; ::_thesis: G . u misses G . v then A90: ( u = 1 or u = 2 ) by A78, FINSEQ_1:2, TARSKI:def_2; percases ( ( u = 1 & v = 2 ) or ( u = 2 & v = 1 ) ) by A78, A88, A89, A90, FINSEQ_1:2, TARSKI:def_2; supposeA91: ( u = 1 & v = 2 ) ; ::_thesis: G . u misses G . v assume G . u meets G . v ; ::_thesis: contradiction then consider z being set such that A92: z in G . u and A93: z in G . v by XBOOLE_0:3; consider A being set such that A94: z in A and A95: A in rng F1 by A86, A91, A92, TARSKI:def_4; consider k9 being set such that A96: k9 in dom F1 and A97: A = F1 . k9 by A95, FUNCT_1:def_3; reconsider k9 = k9 as Element of NAT by A96; A98: z in F . k9 by A94, A96, A97, FUNCT_1:47; k9 in (dom F) /\ (Seg n) by A96, RELAT_1:61; then k9 in Seg n by XBOOLE_0:def_4; then k9 <= n by FINSEQ_1:1; then k9 < n + 1 by NAT_1:13; then A99: F . k9 misses F . (n + 1) by PROB_2:def_2; z in F . (n + 1) by A78, A83, A91, A93; hence contradiction by A99, A98, XBOOLE_0:3; ::_thesis: verum end; supposeA100: ( u = 2 & v = 1 ) ; ::_thesis: G . u misses G . v assume G . u meets G . v ; ::_thesis: contradiction then consider z being set such that A101: z in G . u and A102: z in G . v by XBOOLE_0:3; consider A being set such that A103: z in A and A104: A in rng F1 by A86, A100, A102, TARSKI:def_4; consider k9 being set such that A105: k9 in dom F1 and A106: A = F1 . k9 by A104, FUNCT_1:def_3; reconsider k9 = k9 as Element of NAT by A105; A107: z in F . k9 by A103, A105, A106, FUNCT_1:47; k9 in (dom F) /\ (Seg n) by A105, RELAT_1:61; then k9 in Seg n by XBOOLE_0:def_4; then k9 <= n by FINSEQ_1:1; then k9 < n + 1 by NAT_1:13; then A108: F . k9 misses F . (n + 1) by PROB_2:def_2; z in F . (n + 1) by A78, A83, A100, A101; hence contradiction by A108, A107, XBOOLE_0:3; ::_thesis: verum end; end; end; suppose ( not u in dom G or not v in dom G ) ; ::_thesis: G . u misses G . v then ( G . u = {} or G . v = {} ) by FUNCT_1:def_2; hence G . u misses G . v by XBOOLE_1:65; ::_thesis: verum end; end; end; len G = 2 by A78, FINSEQ_1:def_3; then A109: G = <*(union (rng F1)),(F . (n + 1))*> by A86, A84, FINSEQ_1:44; deffunc H1( Nat) -> Element of ExtREAL = (b . $1) * ((M * G) . $1); consider y being FinSequence of ExtREAL such that A110: ( len y = 2 & ( for m being Nat st m in dom y holds y . m = H1(m) ) ) from FINSEQ_2:sch_1(); A111: dom y = Seg 2 by A110, FINSEQ_1:def_3; 1 in Seg 2 by FINSEQ_1:2, TARSKI:def_2; then A112: y . 1 = (b . 1) * ((M * G) . 1) by A110, A111; consider sumy being Function of NAT,ExtREAL such that A113: Sum y = sumy . (len y) and A114: sumy . 0 = 0. and A115: for k being Element of NAT st k < len y holds sumy . (k + 1) = (sumy . k) + (y . (k + 1)) by EXTREAL1:def_2; A116: sumy . 1 = (sumy . 0) + (y . (0 + 1)) by A110, A115 .= 0. by A80, A112, A114 ; A117: 2 in Seg 2 by FINSEQ_1:2, TARSKI:def_2; then (M * G) . 2 = M . (F . (n + 1)) by A78, A84, FUNCT_1:13 .= (M * F) . (n + 1) by A30, FUNCT_1:13 ; then y . 2 = (a . (n + 1)) * ((M * F) . (n + 1)) by A82, A110, A111, A117; then A118: y . 2 = x . (n + 1) by A7, A8, A30; reconsider G = G as Finite_Sep_Sequence of S by A87, PROB_2:def_2; A119: dom y = dom G by A78, A110, FINSEQ_1:def_3; A120: for k being Nat st k in dom G holds for v being set st v in G . k holds f . v = b . k proof let k be Nat; ::_thesis: ( k in dom G implies for v being set st v in G . k holds f . v = b . k ) assume A121: k in dom G ; ::_thesis: for v being set st v in G . k holds f . v = b . k let v be set ; ::_thesis: ( v in G . k implies f . v = b . k ) assume A122: v in G . k ; ::_thesis: f . v = b . k percases ( k = 1 or k = 2 ) by A78, A121, FINSEQ_1:2, TARSKI:def_2; suppose k = 1 ; ::_thesis: f . v = b . k hence f . v = b . k by A16, A29, A78, A85, A122; ::_thesis: verum end; suppose k = 2 ; ::_thesis: f . v = b . k hence f . v = b . k by A6, A30, A84, A82, A122, MESFUNC3:def_1; ::_thesis: verum end; end; end; A123: for k being Nat st 2 <= k & k in dom b holds ( 0. < b . k & b . k < +infty ) proof let k be Nat; ::_thesis: ( 2 <= k & k in dom b implies ( 0. < b . k & b . k < +infty ) ) assume that A124: 2 <= k and A125: k in dom b ; ::_thesis: ( 0. < b . k & b . k < +infty ) A126: ( k = 1 or k = 2 ) by A73, A125, FINSEQ_1:2, TARSKI:def_2; then G . k <> {} by A4, A6, A11, A29, A31, A84, A124, MESFUNC3:def_1; then consider v being set such that A127: v in G . k by XBOOLE_0:def_1; A128: v in dom f by A6, A16, A29, A31, A84, A124, A126, A127, MESFUNC3:def_1; A129: f . v = b . k by A78, A73, A120, A125, A127; hence 0. < b . k by A5, A68, A82, A124, A126, A128; ::_thesis: b . k < +infty dom f c= X by RELAT_1:def_18; then reconsider v = v as Element of X by A128; |.(f . v).| < +infty by A10, A128, MESFUNC2:def_1; hence b . k < +infty by A129, EXTREAL2:10; ::_thesis: verum end; dom f = (union (rng F1)) \/ (F . (n + 1)) by A6, A31, MESFUNC3:def_1 .= union {(union (rng F1)),(F . (n + 1))} by ZFMISC_1:75 .= union (rng G) by A109, FINSEQ_2:127 ; then A130: G,b are_Re-presentation_of f by A78, A73, A120, MESFUNC3:def_1; Sum y = sumy . (1 + 1) by A110, A113 .= 0. + (x . (n + 1)) by A110, A118, A115, A116 .= x . (n + 1) by XXREAL_3:4 ; hence integral (X,S,M,f) = Sum x by A3, A5, A67, A110, A123, A130, A81, A119, MESFUNC3:def_2; ::_thesis: verum end; caseA131: a . (n + 1) = 0. ; ::_thesis: integral (X,S,M,f) = Sum x defpred S3[ Nat, set ] means ( ( $1 = 1 implies $2 = 0. ) & ( $1 = 2 implies $2 = 1. ) ); defpred S4[ Nat, set ] means ( ( $1 = 1 implies $2 = union (rng F) ) & ( $1 = 2 implies $2 = {} ) ); A132: for k being Nat st k in Seg 2 holds ex v being Element of S st S4[k,v] proof let k be Nat; ::_thesis: ( k in Seg 2 implies ex v being Element of S st S4[k,v] ) assume A133: k in Seg 2 ; ::_thesis: ex v being Element of S st S4[k,v] percases ( k = 1 or k = 2 ) by A133, FINSEQ_1:2, TARSKI:def_2; supposeA134: k = 1 ; ::_thesis: ex v being Element of S st S4[k,v] set v = union (rng F); reconsider v = union (rng F) as Element of S by MESFUNC2:31; take v ; ::_thesis: S4[k,v] thus S4[k,v] by A134; ::_thesis: verum end; supposeA135: k = 2 ; ::_thesis: ex v being Element of S st S4[k,v] reconsider v = {} as Element of S by PROB_1:4; take v ; ::_thesis: S4[k,v] thus S4[k,v] by A135; ::_thesis: verum end; end; end; consider G being FinSequence of S such that A136: ( dom G = Seg 2 & ( for k being Nat st k in Seg 2 holds S4[k,G . k] ) ) from FINSEQ_1:sch_5(A132); A137: for u, v being set st u <> v holds G . u misses G . v proof let u, v be set ; ::_thesis: ( u <> v implies G . u misses G . v ) assume A138: u <> v ; ::_thesis: G . u misses G . v percases ( ( u in dom G & v in dom G ) or not u in dom G or not v in dom G ) ; supposeA139: ( u in dom G & v in dom G ) ; ::_thesis: G . u misses G . v then A140: ( u = 1 or u = 2 ) by A136, FINSEQ_1:2, TARSKI:def_2; percases ( ( u = 1 & v = 2 ) or ( u = 2 & v = 1 ) ) by A136, A138, A139, A140, FINSEQ_1:2, TARSKI:def_2; suppose ( u = 1 & v = 2 ) ; ::_thesis: G . u misses G . v then G . v = {} by A136, A139; hence G . u misses G . v by XBOOLE_1:65; ::_thesis: verum end; suppose ( u = 2 & v = 1 ) ; ::_thesis: G . u misses G . v then G . u = {} by A136, A139; hence G . u misses G . v by XBOOLE_1:65; ::_thesis: verum end; end; end; suppose ( not u in dom G or not v in dom G ) ; ::_thesis: G . u misses G . v then ( G . u = {} or G . v = {} ) by FUNCT_1:def_2; hence G . u misses G . v by XBOOLE_1:65; ::_thesis: verum end; end; end; A141: for k being Nat st k in Seg 2 holds ex v being Element of ExtREAL st S3[k,v] proof let k be Nat; ::_thesis: ( k in Seg 2 implies ex v being Element of ExtREAL st S3[k,v] ) assume A142: k in Seg 2 ; ::_thesis: ex v being Element of ExtREAL st S3[k,v] percases ( k = 1 or k = 2 ) by A142, FINSEQ_1:2, TARSKI:def_2; supposeA143: k = 1 ; ::_thesis: ex v being Element of ExtREAL st S3[k,v] set v = 0. ; reconsider v = 0. as Element of ExtREAL ; take v ; ::_thesis: S3[k,v] thus S3[k,v] by A143; ::_thesis: verum end; supposeA144: k = 2 ; ::_thesis: ex v being Element of ExtREAL st S3[k,v] set v = 1. ; reconsider v = 1. as Element of ExtREAL ; take v ; ::_thesis: S3[k,v] thus S3[k,v] by A144; ::_thesis: verum end; end; end; consider b being FinSequence of ExtREAL such that A145: ( dom b = Seg 2 & ( for k being Nat st k in Seg 2 holds S3[k,b . k] ) ) from FINSEQ_1:sch_5(A141); A146: 2 in dom G by A136, FINSEQ_1:2, TARSKI:def_2; then A147: G . 2 = {} by A136; M . (G . 2) = (M * G) . 2 by A146, FUNCT_1:13; then A148: (M * G) . 2 = 0. by A147, VALUED_0:def_19; 1 in Seg 2 by FINSEQ_1:2, TARSKI:def_2; then A149: G . 1 = union (rng F) by A136; A150: 1 in Seg 2 by FINSEQ_1:2, TARSKI:def_2; then A151: b . 1 = 0. by A145; deffunc H1( Nat) -> Element of ExtREAL = (b . $1) * ((M * G) . $1); consider y being FinSequence of ExtREAL such that A152: ( len y = 2 & ( for k being Nat st k in dom y holds y . k = H1(k) ) ) from FINSEQ_2:sch_1(); A153: dom y = Seg 2 by A152, FINSEQ_1:def_3; 2 in Seg 2 by FINSEQ_1:2, TARSKI:def_2; then A154: y . 2 = (b . 2) * ((M * G) . 2) by A152, A153; 1 in Seg 2 by FINSEQ_1:2, TARSKI:def_2; then A155: y . 1 = (b . 1) * ((M * G) . 1) by A152, A153; reconsider G = G as Finite_Sep_Sequence of S by A137, PROB_2:def_2; A156: dom y = dom G by A136, A152, FINSEQ_1:def_3; A157: for k being Nat st k in dom G holds for v being set st v in G . k holds f . v = b . k proof let k be Nat; ::_thesis: ( k in dom G implies for v being set st v in G . k holds f . v = b . k ) assume A158: k in dom G ; ::_thesis: for v being set st v in G . k holds f . v = b . k let v be set ; ::_thesis: ( v in G . k implies f . v = b . k ) assume A159: v in G . k ; ::_thesis: f . v = b . k percases ( k = 1 or k = 2 ) by A136, A158, FINSEQ_1:2, TARSKI:def_2; supposeA160: k = 1 ; ::_thesis: f . v = b . k then f . v = 0. by A6, A16, A29, A30, A31, A131, A149, A159, MESFUNC3:def_1; hence f . v = b . k by A145, A150, A160; ::_thesis: verum end; suppose k = 2 ; ::_thesis: f . v = b . k hence f . v = b . k by A136, A146, A159; ::_thesis: verum end; end; end; len G = 2 by A136, FINSEQ_1:def_3; then G = <*(union (rng F)),{}*> by A149, A147, FINSEQ_1:44; then rng G = {(union (rng F)),{}} by FINSEQ_2:127; then union (rng G) = (union (rng F)) \/ {} by ZFMISC_1:75 .= dom f by A6, MESFUNC3:def_1 ; then A161: G,b are_Re-presentation_of f by A136, A145, A157, MESFUNC3:def_1; consider sumy being Function of NAT,ExtREAL such that A162: Sum y = sumy . (len y) and A163: sumy . 0 = 0. and A164: for k being Element of NAT st k < len y holds sumy . (k + 1) = (sumy . k) + (y . (k + 1)) by EXTREAL1:def_2; A165: sumy . 1 = (sumy . 0) + (y . (0 + 1)) by A152, A164 .= 0. by A151, A155, A163 ; A166: 2 in Seg 2 by FINSEQ_1:2, TARSKI:def_2; A167: for k being Nat st 2 <= k & k in dom b holds ( 0. < b . k & b . k < +infty ) proof let k be Nat; ::_thesis: ( 2 <= k & k in dom b implies ( 0. < b . k & b . k < +infty ) ) assume that A168: 2 <= k and A169: k in dom b ; ::_thesis: ( 0. < b . k & b . k < +infty ) ( k = 1 or k = 2 ) by A145, A169, FINSEQ_1:2, TARSKI:def_2; hence 0. < b . k by A145, A166, A168, MESFUNC1:def_8; ::_thesis: b . k < +infty S3[k,b . k] by A145, A150, A166; hence b . k < +infty by A145, A169, FINSEQ_1:2, MESFUNC1:def_8, TARSKI:def_2, XXREAL_0:9; ::_thesis: verum end; A170: b . 1 = 0. by A145, A150; ( 1 <= n + 1 & n + 1 <= len x ) by A46, FINSEQ_1:6, NAT_1:11; then n + 1 in dom x by FINSEQ_3:25; then A171: x . (n + 1) = (a . (n + 1)) * ((M * F) . (n + 1)) by A8 .= 0. by A131 ; Sum y = (sumy . 1) + (y . (1 + 1)) by A152, A162, A164 .= 0. by A148, A154, A165 ; hence integral (X,S,M,f) = Sum x by A3, A5, A67, A171, A152, A167, A161, A170, A156, MESFUNC3:def_2; ::_thesis: verum end; end; end; hence integral (X,S,M,f) = Sum x ; ::_thesis: verum end; supposeA172: dom (f | (union (rng (F | (Seg n))))) <> {} ; ::_thesis: integral (X,S,M,f) = Sum x n <= n + 1 by NAT_1:11; then A173: Seg n c= Seg (n + 1) by FINSEQ_1:5; A174: dom F = Seg (n + 1) by A9, FINSEQ_1:def_3; then dom F1 = (Seg (n + 1)) /\ (Seg n) by RELAT_1:61; then A175: dom F1 = Seg n by A173, XBOOLE_1:28; then A176: len F1 = n by FINSEQ_1:def_3; consider G being Finite_Sep_Sequence of S, b, y being FinSequence of ExtREAL such that A177: G,b are_Re-presentation_of f | (union (rng (F | (Seg n)))) and A178: b . 1 = 0. and A179: for n being Nat st 2 <= n & n in dom b holds ( 0. < b . n & b . n < +infty ) and A180: dom y = dom G and A181: for n being Nat st n in dom y holds y . n = (b . n) * ((M * G) . n) and A182: integral (X,S,M,(f | (union (rng (F | (Seg n)))))) = Sum y by A23, A12, MESFUNC3:def_2; A183: for i being Nat st i in dom x1 holds x1 . i = (a1 . i) * ((M * F1) . i) proof let i be Nat; ::_thesis: ( i in dom x1 implies x1 . i = (a1 . i) * ((M * F1) . i) ) assume A184: i in dom x1 ; ::_thesis: x1 . i = (a1 . i) * ((M * F1) . i) A185: dom x1 c= dom x by RELAT_1:60; then x . i = (a . i) * ((M * F) . i) by A8, A184; then A186: x1 . i = (a . i) * ((M * F) . i) by A184, FUNCT_1:47 .= (a1 . i) * ((M * F) . i) by A24, A14, A184, FUNCT_1:47 ; (M * F) . i = M . (F . i) by A7, A184, A185, FUNCT_1:13 .= M . (F1 . i) by A14, A184, FUNCT_1:47 .= (M * F1) . i by A14, A184, FUNCT_1:13 ; hence x1 . i = (a1 . i) * ((M * F1) . i) by A186; ::_thesis: verum end; now__::_thesis:_(_(_(_F_._(n_+_1)_=_{}_or_a_._(n_+_1)_=_0._)_&_integral_(X,S,M,f)_=_Sum_x_)_or_(_F_._(n_+_1)_<>_{}_&_a_._(n_+_1)_<>_0._&_integral_(X,S,M,f)_=_Sum_x_)_) percases ( F . (n + 1) = {} or a . (n + 1) = 0. or ( F . (n + 1) <> {} & a . (n + 1) <> 0. ) ) ; caseA187: ( F . (n + 1) = {} or a . (n + 1) = 0. ) ; ::_thesis: integral (X,S,M,f) = Sum x defpred S2[ Nat, set ] means ( ( $1 = 1 implies $2 = (G . 1) \/ (F . (n + 1)) ) & ( 2 <= $1 implies $2 = G . $1 ) ); A188: for k being Nat st k in Seg (len G) holds ex x being Element of S st S2[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len G) implies ex x being Element of S st S2[k,x] ) A189: rng G c= S by FINSEQ_1:def_4; assume k in Seg (len G) ; ::_thesis: ex x being Element of S st S2[k,x] then k in dom G by FINSEQ_1:def_3; then A190: G . k in rng G by FUNCT_1:3; percases ( k = 1 or k <> 1 ) ; supposeA191: k = 1 ; ::_thesis: ex x being Element of S st S2[k,x] set x = (G . 1) \/ (F . (n + 1)); 1 <= n + 1 by NAT_1:11; then n + 1 in dom F by A9, FINSEQ_3:25; then A192: F . (n + 1) in rng F by FUNCT_1:3; rng F c= S by FINSEQ_1:def_4; then reconsider x = (G . 1) \/ (F . (n + 1)) as Element of S by A190, A189, A191, A192, FINSUB_1:def_1; S2[k,x] by A191; hence ex x being Element of S st S2[k,x] ; ::_thesis: verum end; supposeA193: k <> 1 ; ::_thesis: ex x being Element of S st S2[k,x] set x = G . k; reconsider x = G . k as Element of S by A190, A189; S2[k,x] by A193; hence ex x being Element of S st S2[k,x] ; ::_thesis: verum end; end; end; consider H being FinSequence of S such that A194: ( dom H = Seg (len G) & ( for k being Nat st k in Seg (len G) holds S2[k,H . k] ) ) from FINSEQ_1:sch_5(A188); A195: for u, v being set st u <> v holds H . u misses H . v proof let u, v be set ; ::_thesis: ( u <> v implies H . u misses H . v ) assume A196: u <> v ; ::_thesis: H . u misses H . v percases ( ( u in dom H & v in dom H ) or not u in dom H or not v in dom H ) ; supposeA197: ( u in dom H & v in dom H ) ; ::_thesis: H . u misses H . v then reconsider u1 = u, v1 = v as Element of NAT ; percases ( u = 1 or u <> 1 ) ; supposeA198: u = 1 ; ::_thesis: H . u misses H . v 1 <= v1 by A194, A197, FINSEQ_1:1; then 1 < v1 by A196, A198, XXREAL_0:1; then A199: 1 + 1 <= v1 by NAT_1:13; then A200: H . v = G . v by A194, A197; A201: F . (n + 1) misses G . v proof percases ( F . (n + 1) = {} or a . (n + 1) = 0. ) by A187; suppose F . (n + 1) = {} ; ::_thesis: F . (n + 1) misses G . v hence F . (n + 1) misses G . v by XBOOLE_1:65; ::_thesis: verum end; supposeA202: a . (n + 1) = 0. ; ::_thesis: F . (n + 1) misses G . v assume F . (n + 1) meets G . v ; ::_thesis: contradiction then consider w being set such that A203: w in F . (n + 1) and A204: w in G . v by XBOOLE_0:3; A205: v1 in dom G by A194, A197, FINSEQ_1:def_3; then A206: v1 in dom b by A177, MESFUNC3:def_1; G . v1 in rng G by A205, FUNCT_1:3; then w in union (rng G) by A204, TARSKI:def_4; then w in dom (f | (union (rng (F | (Seg n))))) by A177, MESFUNC3:def_1; then A207: f . w = (f | (union (rng (F | (Seg n))))) . w by FUNCT_1:47 .= b . v1 by A177, A204, A205, MESFUNC3:def_1 ; 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 A9, FINSEQ_1:def_3; then f . w = 0. by A6, A202, A203, MESFUNC3:def_1; hence contradiction by A179, A199, A207, A206; ::_thesis: verum end; end; end; ( H . u = (G . 1) \/ (F . (n + 1)) & G . 1 misses G . v ) by A194, A196, A197, A198, PROB_2:def_2; hence H . u misses H . v by A200, A201, XBOOLE_1:70; ::_thesis: verum end; supposeA208: u <> 1 ; ::_thesis: H . u misses H . v 1 <= u1 by A194, A197, FINSEQ_1:1; then 1 < u1 by A208, XXREAL_0:1; then A209: 1 + 1 <= u1 by NAT_1:13; then A210: H . u = G . u by A194, A197; percases ( v = 1 or v <> 1 ) ; supposeA211: v = 1 ; ::_thesis: H . u misses H . v A212: F . (n + 1) misses G . u proof percases ( F . (n + 1) = {} or a . (n + 1) = 0. ) by A187; suppose F . (n + 1) = {} ; ::_thesis: F . (n + 1) misses G . u hence F . (n + 1) misses G . u by XBOOLE_1:65; ::_thesis: verum end; supposeA213: a . (n + 1) = 0. ; ::_thesis: F . (n + 1) misses G . u assume F . (n + 1) meets G . u ; ::_thesis: contradiction then consider w being set such that A214: w in F . (n + 1) and A215: w in G . u by XBOOLE_0:3; A216: u1 in dom G by A194, A197, FINSEQ_1:def_3; then A217: u1 in dom b by A177, MESFUNC3:def_1; G . u1 in rng G by A216, FUNCT_1:3; then w in union (rng G) by A215, TARSKI:def_4; then w in dom (f | (union (rng (F | (Seg n))))) by A177, MESFUNC3:def_1; then A218: f . w = (f | (union (rng (F | (Seg n))))) . w by FUNCT_1:47 .= b . u1 by A177, A215, A216, MESFUNC3:def_1 ; 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 A9, FINSEQ_1:def_3; then f . w = 0. by A6, A213, A214, MESFUNC3:def_1; hence contradiction by A179, A209, A218, A217; ::_thesis: verum end; end; end; ( H . v = (G . 1) \/ (F . (n + 1)) & G . 1 misses G . u ) by A194, A196, A197, A211, PROB_2:def_2; hence H . u misses H . v by A210, A212, XBOOLE_1:70; ::_thesis: verum end; supposeA219: v <> 1 ; ::_thesis: H . u misses H . v 1 <= v1 by A194, A197, FINSEQ_1:1; then 1 < v1 by A219, XXREAL_0:1; then 1 + 1 <= v1 by NAT_1:13; then H . v = G . v by A194, A197; hence H . u misses H . v by A196, A210, PROB_2:def_2; ::_thesis: verum end; end; end; end; end; suppose ( not u in dom H or not v in dom H ) ; ::_thesis: H . u misses H . v then ( H . u = {} or H . v = {} ) by FUNCT_1:def_2; hence H . u misses H . v by XBOOLE_1:65; ::_thesis: verum end; end; end; deffunc H1( Nat) -> Element of ExtREAL = (b . $1) * ((M * H) . $1); reconsider H = H as Finite_Sep_Sequence of S by A195, PROB_2:def_2; consider z being FinSequence of ExtREAL such that A220: ( len z = len y & ( for n being Nat st n in dom z holds z . n = H1(n) ) ) from FINSEQ_2:sch_1(); G <> {} by A172, A177, MESFUNC3:def_1, RELAT_1:38, ZFMISC_1:2; then 0 + 1 <= len G by NAT_1:13; then A221: 1 in Seg (len G) by FINSEQ_1:1; A222: dom f = union (rng H) proof thus dom f c= union (rng H) :: according to XBOOLE_0:def_10 ::_thesis: union (rng H) c= dom f proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in dom f or v in union (rng H) ) assume v in dom f ; ::_thesis: v in union (rng H) then v in union (rng F) by A6, MESFUNC3:def_1; then consider A being set such that A223: v in A and A224: A in rng F by TARSKI:def_4; consider u being set such that A225: u in dom F and A226: A = F . u by A224, FUNCT_1:def_3; reconsider u = u as Element of NAT by A225; A227: u in Seg (len F) by A225, FINSEQ_1:def_3; then A228: 1 <= u by FINSEQ_1:1; A229: u <= n + 1 by A9, A227, FINSEQ_1:1; percases ( u = n + 1 or u <> n + 1 ) ; suppose u = n + 1 ; ::_thesis: v in union (rng H) then H . 1 = (G . 1) \/ A by A194, A221, A226; then A230: v in H . 1 by A223, XBOOLE_0:def_3; H . 1 in rng H by A194, A221, FUNCT_1:3; hence v in union (rng H) by A230, TARSKI:def_4; ::_thesis: verum end; suppose u <> n + 1 ; ::_thesis: v in union (rng H) then u < n + 1 by A229, XXREAL_0:1; then u <= n by NAT_1:13; then u in Seg n by A228, FINSEQ_1:1; then ( F1 . u in rng F1 & A = F1 . u ) by A175, A226, FUNCT_1:3, FUNCT_1:47; then v in union (rng F1) by A223, TARSKI:def_4; then v in union (rng G) by A16, A177, MESFUNC3:def_1; then consider B being set such that A231: v in B and A232: B in rng G by TARSKI:def_4; consider w being set such that A233: w in dom G and A234: B = G . w by A232, FUNCT_1:def_3; reconsider w = w as Element of NAT by A233; A235: w in Seg (len G) by A233, FINSEQ_1:def_3; percases ( w = 1 or w <> 1 ) ; supposeA236: w = 1 ; ::_thesis: v in union (rng H) H . 1 = (G . 1) \/ (F . (n + 1)) by A194, A221; then A237: v in H . 1 by A231, A234, A236, XBOOLE_0:def_3; H . 1 in rng H by A194, A221, FUNCT_1:3; hence v in union (rng H) by A237, TARSKI:def_4; ::_thesis: verum end; supposeA238: w <> 1 ; ::_thesis: v in union (rng H) 1 <= w by A233, FINSEQ_3:25; then 1 < w by A238, XXREAL_0:1; then 1 + 1 <= w by NAT_1:13; then A239: v in H . w by A194, A231, A234, A235; H . w in rng H by A194, A235, FUNCT_1:3; hence v in union (rng H) by A239, TARSKI:def_4; ::_thesis: verum end; end; end; end; end; let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in union (rng H) or v in dom f ) assume v in union (rng H) ; ::_thesis: v in dom f then consider A being set such that A240: v in A and A241: A in rng H by TARSKI:def_4; consider k being set such that A242: k in dom H and A243: A = H . k by A241, FUNCT_1:def_3; reconsider k = k as Element of NAT by A242; percases ( k = 1 or k <> 1 ) ; suppose k = 1 ; ::_thesis: v in dom f then A244: H . k = (G . 1) \/ (F . (n + 1)) by A194, A242; percases ( v in G . 1 or v in F . (n + 1) ) by A240, A243, A244, XBOOLE_0:def_3; supposeA245: v in G . 1 ; ::_thesis: v in dom f 1 in dom G by A221, FINSEQ_1:def_3; then G . 1 in rng G by FUNCT_1:3; then v in union (rng G) by A245, TARSKI:def_4; then v in dom (f | (union (rng (F | (Seg n))))) by A177, MESFUNC3:def_1; then v in (dom f) /\ (union (rng F1)) by RELAT_1:61; hence v in dom f by XBOOLE_0:def_4; ::_thesis: verum end; supposeA246: v in F . (n + 1) ; ::_thesis: v in dom f 1 <= n + 1 by NAT_1:11; then n + 1 in dom F by A9, FINSEQ_3:25; then F . (n + 1) in rng F by FUNCT_1:3; then v in union (rng F) by A246, TARSKI:def_4; hence v in dom f by A6, MESFUNC3:def_1; ::_thesis: verum end; end; end; supposeA247: k <> 1 ; ::_thesis: v in dom f 1 <= k by A194, A242, FINSEQ_1:1; then 1 < k by A247, XXREAL_0:1; then 1 + 1 <= k by NAT_1:13; then A248: v in G . k by A194, A240, A242, A243; k in dom G by A194, A242, FINSEQ_1:def_3; then G . k in rng G by FUNCT_1:3; then v in union (rng G) by A248, TARSKI:def_4; then v in dom (f | (union (rng (F | (Seg n))))) by A177, MESFUNC3:def_1; then v in (dom f) /\ (union (rng F1)) by RELAT_1:61; hence v in dom f by XBOOLE_0:def_4; ::_thesis: verum end; end; end; A249: now__::_thesis:_not_-infty_in_rng_x1 assume -infty in rng x1 ; ::_thesis: contradiction then consider l being set such that A250: l in dom x1 and A251: x1 . l = -infty by FUNCT_1:def_3; reconsider l = l as Element of NAT by A250; l in (dom x) /\ (Seg n) by A250, RELAT_1:61; then A252: l in dom x by XBOOLE_0:def_4; x . l = -infty by A250, A251, FUNCT_1:47; then A253: (a . l) * ((M * F) . l) = -infty by A8, A252; percases ( F . l <> {} or F . l = {} ) ; supposeA254: F . l <> {} ; ::_thesis: contradiction reconsider EMPTY = {} as Element of S by MEASURE1:7; consider v being set such that A255: v in F . l by A254, XBOOLE_0:def_1; A256: F . l in rng F by A7, A252, FUNCT_1:3; then v in union (rng F) by A255, TARSKI:def_4; then A257: v in dom f by A6, MESFUNC3:def_1; rng F c= S by FINSEQ_1:def_4; then reconsider Fl = F . l as Element of S by A256; EMPTY c= F . l by XBOOLE_1:2; then M . {} <= M . Fl by MEASURE1:31; then 0. <= M . Fl by VALUED_0:def_19; then A258: 0. <= (M * F) . l by A7, A252, FUNCT_1:13; a . l = f . v by A6, A7, A252, A255, MESFUNC3:def_1; then 0. <= a . l by A5, A257; hence contradiction by A253, A258; ::_thesis: verum end; supposeA259: F . l = {} ; ::_thesis: contradiction (M * F) . l = M . (F . l) by A7, A252, FUNCT_1:13 .= 0. by A259, VALUED_0:def_19 ; hence contradiction by A253; ::_thesis: verum end; end; end; 1 <= n + 1 by NAT_1:11; then A260: n + 1 in dom F by A9, FINSEQ_3:25; A261: x . (n + 1) = 0. proof percases ( F . (n + 1) = {} or a . (n + 1) = 0. ) by A187; supposeA262: F . (n + 1) = {} ; ::_thesis: x . (n + 1) = 0. (M * F) . (n + 1) = M . (F . (n + 1)) by A260, FUNCT_1:13; then A263: (M * F) . (n + 1) = 0. by A262, VALUED_0:def_19; x . (n + 1) = (a . (n + 1)) * ((M * F) . (n + 1)) by A7, A8, A260; hence x . (n + 1) = 0. by A263; ::_thesis: verum end; supposeA264: a . (n + 1) = 0. ; ::_thesis: x . (n + 1) = 0. x . (n + 1) = (a . (n + 1)) * ((M * F) . (n + 1)) by A7, A8, A260; hence x . (n + 1) = 0. by A264; ::_thesis: verum end; end; end; A265: now__::_thesis:_not_-infty_in_rng_<*(x_._(n_+_1))*> assume -infty in rng <*(x . (n + 1))*> ; ::_thesis: contradiction then -infty in {(x . (n + 1))} by FINSEQ_1:39; hence contradiction by A261; ::_thesis: verum end; A266: for m being Nat st m in dom H holds for x being set st x in H . m holds f . x = b . m proof let m be Nat; ::_thesis: ( m in dom H implies for x being set st x in H . m holds f . x = b . m ) assume A267: m in dom H ; ::_thesis: for x being set st x in H . m holds f . x = b . m let x be set ; ::_thesis: ( x in H . m implies f . x = b . m ) assume A268: x in H . m ; ::_thesis: f . x = b . m percases ( m = 1 or m <> 1 ) ; supposeA269: m = 1 ; ::_thesis: f . x = b . m then A270: H . m = (G . 1) \/ (F . (n + 1)) by A194, A267; percases ( x in G . 1 or x in F . (n + 1) ) by A268, A270, XBOOLE_0:def_3; supposeA271: x in G . 1 ; ::_thesis: f . x = b . m A272: m in dom G by A194, A267, FINSEQ_1:def_3; then G . 1 in rng G by A269, FUNCT_1:3; then x in union (rng G) by A271, TARSKI:def_4; then A273: x in dom (f | (union (rng (F | (Seg n))))) by A177, MESFUNC3:def_1; (f | (union (rng (F | (Seg n))))) . x = b . m by A177, A269, A271, A272, MESFUNC3:def_1; hence f . x = b . m by A273, FUNCT_1:47; ::_thesis: verum end; supposeA274: x in F . (n + 1) ; ::_thesis: f . x = b . m 1 <= n + 1 by NAT_1:11; then n + 1 in dom F by A9, FINSEQ_3:25; hence f . x = b . m by A6, A178, A187, A269, A274, MESFUNC3:def_1; ::_thesis: verum end; end; end; supposeA275: m <> 1 ; ::_thesis: f . x = b . m 1 <= m by A267, FINSEQ_3:25; then 1 < m by A275, XXREAL_0:1; then 1 + 1 <= m by NAT_1:13; then A276: H . m = G . m by A194, A267; A277: m in dom G by A194, A267, FINSEQ_1:def_3; then G . m in rng G by FUNCT_1:3; then x in union (rng G) by A268, A276, TARSKI:def_4; then A278: x in dom (f | (union (rng (F | (Seg n))))) by A177, MESFUNC3:def_1; (f | (union (rng (F | (Seg n))))) . x = b . m by A177, A268, A277, A276, MESFUNC3:def_1; hence f . x = b . m by A278, FUNCT_1:47; ::_thesis: verum end; end; end; A279: dom z = dom y by A220, FINSEQ_3:29; then A280: dom z = dom H by A180, A194, FINSEQ_1:def_3; A281: for k being Nat st k in dom z holds z . k = y . k proof let k be Nat; ::_thesis: ( k in dom z implies z . k = y . k ) assume A282: k in dom z ; ::_thesis: z . k = y . k then A283: z . k = (b . k) * ((M * H) . k) by A220; A284: y . k = (b . k) * ((M * G) . k) by A181, A279, A282; percases ( k = 1 or k <> 1 ) ; supposeA285: k = 1 ; ::_thesis: z . k = y . k then z . k = 0. by A178, A283; hence z . k = y . k by A178, A284, A285; ::_thesis: verum end; supposeA286: k <> 1 ; ::_thesis: z . k = y . k A287: k in Seg (len G) by A180, A279, A282, FINSEQ_1:def_3; then 1 <= k by FINSEQ_1:1; then 1 < k by A286, XXREAL_0:1; then A288: 1 + 1 <= k by NAT_1:13; (M * H) . k = M . (H . k) by A280, A282, FUNCT_1:13 .= M . (G . k) by A194, A287, A288 .= (M * G) . k by A180, A279, A282, FUNCT_1:13 ; hence z . k = y . k by A181, A279, A282, A283; ::_thesis: verum end; end; end; len x = n + 1 by A7, A9, FINSEQ_3:29; then x = x | (n + 1) by FINSEQ_1:58 .= x | (Seg (n + 1)) by FINSEQ_1:def_15 .= x1 ^ <*(x . (n + 1))*> by A7, A260, FINSEQ_5:10 ; then A289: Sum x = (Sum x1) + (Sum <*(x . (n + 1))*>) by A249, A265, EXTREAL1:10 .= (Sum x1) + 0. by A261, EXTREAL1:8 ; dom H = dom G by A194, FINSEQ_1:def_3 .= dom b by A177, MESFUNC3:def_1 ; then H,b are_Re-presentation_of f by A222, A266, MESFUNC3:def_1; then integral (X,S,M,f) = Sum z by A3, A5, A178, A179, A220, A280, MESFUNC3:def_2 .= integral (X,S,M,(f | (union (rng (F | (Seg n)))))) by A182, A279, A281, FINSEQ_1:13 .= Sum x1 by A2, A23, A12, A28, A14, A172, A183, A176 .= Sum x by A289, XXREAL_3:4 ; hence integral (X,S,M,f) = Sum x ; ::_thesis: verum end; caseA290: ( F . (n + 1) <> {} & a . (n + 1) <> 0. ) ; ::_thesis: integral (X,S,M,f) = Sum x defpred S2[ Nat, set ] means ( ( $1 <= len b implies $2 = b . $1 ) & ( $1 = (len b) + 1 implies $2 = a . (n + 1) ) ); A291: f is V63() by A3, MESFUNC2:def_4; consider v being set such that A292: v in F . (n + 1) by A290, XBOOLE_0:def_1; A293: for k being Nat st k in Seg ((len b) + 1) holds ex v being Element of ExtREAL st S2[k,v] proof let k be Nat; ::_thesis: ( k in Seg ((len b) + 1) implies ex v being Element of ExtREAL st S2[k,v] ) assume k in Seg ((len b) + 1) ; ::_thesis: ex v being Element of ExtREAL st S2[k,v] percases ( k <> (len b) + 1 or k = (len b) + 1 ) ; supposeA294: k <> (len b) + 1 ; ::_thesis: ex v being Element of ExtREAL st S2[k,v] reconsider v = b . k as Element of ExtREAL ; take v ; ::_thesis: S2[k,v] thus S2[k,v] by A294; ::_thesis: verum end; supposeA295: k = (len b) + 1 ; ::_thesis: ex v being Element of ExtREAL st S2[k,v] reconsider v = a . (n + 1) as Element of ExtREAL ; take v ; ::_thesis: S2[k,v] thus S2[k,v] by A295, NAT_1:13; ::_thesis: verum end; end; end; consider c being FinSequence of ExtREAL such that A296: ( dom c = Seg ((len b) + 1) & ( for k being Nat st k in Seg ((len b) + 1) holds S2[k,c . k] ) ) from FINSEQ_1:sch_5(A293); 1 <= n + 1 by NAT_1:11; then A297: n + 1 in dom F by A9, FINSEQ_3:25; then F . (n + 1) in rng F by FUNCT_1:3; then v in union (rng F) by A292, TARSKI:def_4; then A298: v in dom f by A6, MESFUNC3:def_1; dom f c= X by RELAT_1:def_18; then reconsider v = v as Element of X by A298; f . v = a . (n + 1) by A6, A297, A292, MESFUNC3:def_1; then |.(a . (n + 1)).| < +infty by A291, A298, MESFUNC2:def_1; then A299: a . (n + 1) < +infty by EXTREAL2:10; A300: len c = (len b) + 1 by A296, FINSEQ_1:def_3; A301: 0. <= f . v by A5, A298; then A302: 0. < a . (n + 1) by A6, A290, A297, A292, MESFUNC3:def_1; A303: for m being Nat st 2 <= m & m in dom c holds ( 0. < c . m & c . m < +infty ) proof let m be Nat; ::_thesis: ( 2 <= m & m in dom c implies ( 0. < c . m & c . m < +infty ) ) assume that A304: 2 <= m and A305: m in dom c ; ::_thesis: ( 0. < c . m & c . m < +infty ) A306: m <= len c by A305, FINSEQ_3:25; percases ( m = len c or m <> len c ) ; suppose m = len c ; ::_thesis: ( 0. < c . m & c . m < +infty ) hence ( 0. < c . m & c . m < +infty ) by A302, A299, A296, A300, A305; ::_thesis: verum end; suppose m <> len c ; ::_thesis: ( 0. < c . m & c . m < +infty ) then m < (len b) + 1 by A300, A306, XXREAL_0:1; then A307: m <= len b by NAT_1:13; 1 <= m by A304, XXREAL_0:2; then A308: m in dom b by A307, FINSEQ_3:25; c . m = b . m by A296, A305, A307; hence ( 0. < c . m & c . m < +infty ) by A179, A304, A308; ::_thesis: verum end; end; end; A309: 0. <= a . (n + 1) by A6, A297, A292, A301, MESFUNC3:def_1; A310: now__::_thesis:_(_not_-infty_in_rng_y_&_not_-infty_in_rng_<*((a_._(n_+_1))_*_((M_*_F)_._(n_+_1)))*>_) assume A311: ( -infty in rng y or -infty in rng <*((a . (n + 1)) * ((M * F) . (n + 1)))*> ) ; ::_thesis: contradiction percases ( -infty in rng y or -infty in rng <*((a . (n + 1)) * ((M * F) . (n + 1)))*> ) by A311; suppose -infty in rng y ; ::_thesis: contradiction then consider k being set such that A312: k in dom y and A313: -infty = y . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A312; A314: y . k = (b . k) * ((M * G) . k) by A181, A312; k in Seg (len y) by A312, FINSEQ_1:def_3; then A315: 1 <= k by FINSEQ_1:1; percases ( k = 1 or k <> 1 ) ; suppose k = 1 ; ::_thesis: contradiction hence contradiction by A178, A313, A314; ::_thesis: verum end; suppose k <> 1 ; ::_thesis: contradiction then 1 < k by A315, XXREAL_0:1; then A316: 1 + 1 <= k by NAT_1:13; k in dom b by A177, A180, A312, MESFUNC3:def_1; then A317: 0. < b . k by A179, A316; ( G . k in rng G & rng G c= S ) by A180, A312, FINSEQ_1:def_4, FUNCT_1:3; then reconsider Gk = G . k as Element of S ; reconsider EMPTY = {} as Element of S by PROB_1:4; M . EMPTY <= M . Gk by MEASURE1:31, XBOOLE_1:2; then A318: 0. <= M . Gk by VALUED_0:def_19; (M * G) . k = M . (G . k) by A180, A312, FUNCT_1:13; hence contradiction by A313, A314, A317, A318; ::_thesis: verum end; end; end; supposeA319: -infty in rng <*((a . (n + 1)) * ((M * F) . (n + 1)))*> ; ::_thesis: contradiction reconsider EMPTY = {} as Element of S by PROB_1:4; A320: rng F c= S by FINSEQ_1:def_4; 1 <= n + 1 by NAT_1:11; then A321: n + 1 in dom F by A9, FINSEQ_3:25; then F . (n + 1) in rng F by FUNCT_1:3; then reconsider Fn1 = F . (n + 1) as Element of S by A320; A322: (M * F) . (n + 1) = M . Fn1 by A321, FUNCT_1:13; M . EMPTY <= M . Fn1 by MEASURE1:31, XBOOLE_1:2; then A323: 0. <= M . Fn1 by VALUED_0:def_19; -infty in {((a . (n + 1)) * ((M * F) . (n + 1)))} by A319, FINSEQ_1:38; hence contradiction by A309, A323, A322, TARSKI:def_1; ::_thesis: verum end; end; end; A324: not -infty in rng x1 proof reconsider EMPTY = {} as Element of S by PROB_1:4; assume -infty in rng x1 ; ::_thesis: contradiction then consider k being set such that A325: k in dom x1 and A326: -infty = x1 . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A325; k in (dom x) /\ (Seg n) by A325, RELAT_1:61; then A327: k in dom x by XBOOLE_0:def_4; then A328: x . k = (a . k) * ((M * F) . k) by A8; A329: F . k in rng F by A7, A327, FUNCT_1:3; rng F c= S by FINSEQ_1:def_4; then reconsider Fk = F . k as Element of S by A329; percases ( F . k <> {} or F . k = {} ) ; suppose F . k <> {} ; ::_thesis: contradiction then consider v being set such that A330: v in F . k by XBOOLE_0:def_1; v in union (rng F) by A329, A330, TARSKI:def_4; then A331: v in dom f by A6, MESFUNC3:def_1; a . k = f . v by A6, A7, A327, A330, MESFUNC3:def_1; then A332: 0. <= a . k by A5, A331; M . EMPTY <= M . Fk by MEASURE1:31, XBOOLE_1:2; then A333: 0. <= M . Fk by VALUED_0:def_19; M . Fk = (M * F) . k by A7, A327, FUNCT_1:13; hence contradiction by A325, A326, A328, A332, A333, FUNCT_1:47; ::_thesis: verum end; suppose F . k = {} ; ::_thesis: contradiction then 0. = M . (F . k) by VALUED_0:def_19 .= (M * F) . k by A7, A327, FUNCT_1:13 ; hence contradiction by A325, A326, A328, FUNCT_1:47; ::_thesis: verum end; end; end; defpred S3[ Nat, set ] means ( ( $1 <= len G implies $2 = G . $1 ) & ( $1 = (len G) + 1 implies $2 = F . (n + 1) ) ); A334: dom G = dom b by A177, MESFUNC3:def_1; A335: Seg (len G) = dom G by FINSEQ_1:def_3 .= Seg (len b) by A334, FINSEQ_1:def_3 ; then A336: len G = len b by FINSEQ_1:6; A337: for k being Nat st k in Seg ((len G) + 1) holds ex v being Element of S st S3[k,v] proof let k be Nat; ::_thesis: ( k in Seg ((len G) + 1) implies ex v being Element of S st S3[k,v] ) assume A338: k in Seg ((len G) + 1) ; ::_thesis: ex v being Element of S st S3[k,v] percases ( k <> (len G) + 1 or k = (len G) + 1 ) ; supposeA339: k <> (len G) + 1 ; ::_thesis: ex v being Element of S st S3[k,v] k <= (len G) + 1 by A338, FINSEQ_1:1; then k < (len G) + 1 by A339, XXREAL_0:1; then A340: k <= len G by NAT_1:13; 1 <= k by A338, FINSEQ_1:1; then k in dom G by A340, FINSEQ_3:25; then A341: G . k in rng G by FUNCT_1:3; rng G c= S by FINSEQ_1:def_4; then reconsider v = G . k as Element of S by A341; take v ; ::_thesis: S3[k,v] thus S3[k,v] by A339; ::_thesis: verum end; supposeA342: k = (len G) + 1 ; ::_thesis: ex v being Element of S st S3[k,v] ( F . (n + 1) in rng F & rng F c= S ) by A297, FINSEQ_1:def_4, FUNCT_1:3; then reconsider v = F . (n + 1) as Element of S ; take v ; ::_thesis: S3[k,v] thus S3[k,v] by A342, NAT_1:13; ::_thesis: verum end; end; end; consider H being FinSequence of S such that A343: ( dom H = Seg ((len G) + 1) & ( for k being Nat st k in Seg ((len G) + 1) holds S3[k,H . k] ) ) from FINSEQ_1:sch_5(A337); A344: for i, j being set st i <> j holds H . i misses H . j proof let i, j be set ; ::_thesis: ( i <> j implies H . i misses H . j ) assume A345: i <> j ; ::_thesis: H . i misses H . j percases ( ( i in dom H & j in dom H ) or not i in dom H or not j in dom H ) ; supposeA346: ( i in dom H & j in dom H ) ; ::_thesis: H . i misses H . j then reconsider i = i, j = j as Element of NAT ; A347: 1 <= i by A343, A346, FINSEQ_1:1; A348: j <= (len G) + 1 by A343, A346, FINSEQ_1:1; A349: for k being Nat st 1 <= k & k <= len G holds H . k misses F . (n + 1) proof A350: union (rng F1) misses F . (n + 1) proof assume union (rng F1) meets F . (n + 1) ; ::_thesis: contradiction then consider v being set such that A351: v in union (rng F1) and A352: v in F . (n + 1) by XBOOLE_0:3; consider A being set such that A353: v in A and A354: A in rng F1 by A351, TARSKI:def_4; consider m being set such that A355: m in dom F1 and A356: A = F1 . m by A354, FUNCT_1:def_3; reconsider m = m as Element of NAT by A355; m in Seg (len F1) by A355, FINSEQ_1:def_3; then m <= n by A176, FINSEQ_1:1; then A357: m <> n + 1 by NAT_1:13; F1 . m = F . m by A355, FUNCT_1:47; then A misses F . (n + 1) by A356, A357, PROB_2:def_2; then A /\ (F . (n + 1)) = {} by XBOOLE_0:def_7; hence contradiction by A352, A353, XBOOLE_0:def_4; ::_thesis: verum end; let k be Nat; ::_thesis: ( 1 <= k & k <= len G implies H . k misses F . (n + 1) ) assume that A358: 1 <= k and A359: k <= len G ; ::_thesis: H . k misses F . (n + 1) k in dom G by A358, A359, FINSEQ_3:25; then G . k c= union (rng G) by FUNCT_1:3, ZFMISC_1:74; then G . k c= dom (f | (union (rng (F | (Seg n))))) by A177, MESFUNC3:def_1; then A360: G . k c= (dom f) /\ (union (rng F1)) by RELAT_1:61; k <= (len G) + 1 by A359, NAT_1:12; then k in Seg ((len G) + 1) by A358, FINSEQ_1:1; then H . k = G . k by A343, A359; hence H . k misses F . (n + 1) by A360, A350, XBOOLE_1:18, XBOOLE_1:63; ::_thesis: verum end; A361: 1 <= j by A343, A346, FINSEQ_1:1; A362: i <= (len G) + 1 by A343, A346, FINSEQ_1:1; A363: S3[i,H . i] by A343, A346; A364: S3[j,H . j] by A343, A346; percases ( i = (len G) + 1 or i <> (len G) + 1 ) ; supposeA365: i = (len G) + 1 ; ::_thesis: H . i misses H . j then j < (len G) + 1 by A345, A348, XXREAL_0:1; then j <= len G by NAT_1:13; hence H . i misses H . j by A361, A363, A349, A365; ::_thesis: verum end; suppose i <> (len G) + 1 ; ::_thesis: H . i misses H . j then A366: i < (len G) + 1 by A362, XXREAL_0:1; then A367: i <= len G by NAT_1:13; percases ( j = (len G) + 1 or j <> (len G) + 1 ) ; suppose j = (len G) + 1 ; ::_thesis: H . i misses H . j hence H . i misses H . j by A347, A364, A349, A367; ::_thesis: verum end; suppose j <> (len G) + 1 ; ::_thesis: H . i misses H . j then j < (len G) + 1 by A348, XXREAL_0:1; hence H . i misses H . j by A345, A363, A364, A366, NAT_1:13, PROB_2:def_2; ::_thesis: verum end; end; end; end; end; supposeA368: ( not i in dom H or not j in dom H ) ; ::_thesis: H . i misses H . j percases ( not i in dom H or not j in dom H ) by A368; suppose not i in dom H ; ::_thesis: H . i misses H . j then H . i = {} by FUNCT_1:def_2; hence H . i misses H . j by XBOOLE_1:65; ::_thesis: verum end; suppose not j in dom H ; ::_thesis: H . i misses H . j then H . j = {} by FUNCT_1:def_2; hence H . i misses H . j by XBOOLE_1:65; ::_thesis: verum end; end; end; end; end; A369: len H = (len G) + 1 by A343, FINSEQ_1:def_3; A370: Seg (len H) = Seg ((len G) + 1) by A343, FINSEQ_1:def_3; defpred S4[ Nat, set ] means ( ( $1 <= len y implies $2 = (b . $1) * ((M * H) . $1) ) & ( $1 = (len y) + 1 implies $2 = (a . (n + 1)) * ((M * F) . (n + 1)) ) ); A371: for k being Nat st k in Seg ((len y) + 1) holds ex v being Element of ExtREAL st S4[k,v] proof let k be Nat; ::_thesis: ( k in Seg ((len y) + 1) implies ex v being Element of ExtREAL st S4[k,v] ) assume k in Seg ((len y) + 1) ; ::_thesis: ex v being Element of ExtREAL st S4[k,v] percases ( k <> (len y) + 1 or k = (len y) + 1 ) ; supposeA372: k <> (len y) + 1 ; ::_thesis: ex v being Element of ExtREAL st S4[k,v] reconsider v = (b . k) * ((M * H) . k) as Element of ExtREAL ; take v ; ::_thesis: S4[k,v] thus S4[k,v] by A372; ::_thesis: verum end; supposeA373: k = (len y) + 1 ; ::_thesis: ex v being Element of ExtREAL st S4[k,v] reconsider v = (a . (n + 1)) * ((M * F) . (n + 1)) as Element of ExtREAL ; take v ; ::_thesis: S4[k,v] thus S4[k,v] by A373, NAT_1:13; ::_thesis: verum end; end; end; consider z being FinSequence of ExtREAL such that A374: ( dom z = Seg ((len y) + 1) & ( for k being Nat st k in Seg ((len y) + 1) holds S4[k,z . k] ) ) from FINSEQ_1:sch_5(A371); A375: len y = len G by A180, FINSEQ_3:29; then A376: len z = (len G) + 1 by A374, FINSEQ_1:def_3; then A377: len z in dom H by A343, FINSEQ_1:4; A378: len z in Seg ((len G) + 1) by A376, FINSEQ_1:4; A379: (M * F) . (n + 1) = M . (F . (n + 1)) by A174, FINSEQ_1:4, FUNCT_1:13 .= M . (H . (len z)) by A343, A376, A378 .= (M * H) . (len z) by A377, FUNCT_1:13 ; A380: for m being Nat st m in dom z holds z . m = (c . m) * ((M * H) . m) proof let m be Nat; ::_thesis: ( m in dom z implies z . m = (c . m) * ((M * H) . m) ) assume A381: m in dom z ; ::_thesis: z . m = (c . m) * ((M * H) . m) then A382: S2[m,c . m] by A296, A336, A374, A375; percases ( m = (len y) + 1 or m <> (len y) + 1 ) ; suppose m = (len y) + 1 ; ::_thesis: z . m = (c . m) * ((M * H) . m) hence z . m = (c . m) * ((M * H) . m) by A335, A374, A375, A376, A379, A381, A382, FINSEQ_1:6; ::_thesis: verum end; supposeA383: m <> (len y) + 1 ; ::_thesis: z . m = (c . m) * ((M * H) . m) m <= (len y) + 1 by A374, A381, FINSEQ_1:1; then m < (len y) + 1 by A383, XXREAL_0:1; then A384: m <= len b by A336, A375, NAT_1:13; then c . m = b . m by A296, A336, A374, A375, A381; hence z . m = (c . m) * ((M * H) . m) by A336, A374, A375, A381, A384; ::_thesis: verum end; end; end; reconsider H = H as Finite_Sep_Sequence of S by A344, PROB_2:def_2; A385: len G = len y by A180, FINSEQ_3:29; A386: len z = (len y) + 1 by A374, FINSEQ_1:def_3; then len z in Seg ((len y) + 1) by FINSEQ_1:4; then A387: z . (len z) = (a . (n + 1)) * ((M * F) . (n + 1)) by A374, A386; A388: for k being Nat st 1 <= k & k <= len z holds z . k = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len z implies z . k = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k ) assume that A389: 1 <= k and A390: k <= len z ; ::_thesis: z . k = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k percases ( k = len z or k <> len z ) ; suppose k = len z ; ::_thesis: z . k = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k hence z . k = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k by A386, A387, FINSEQ_1:42; ::_thesis: verum end; suppose k <> len z ; ::_thesis: z . k = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k then k < len z by A390, XXREAL_0:1; then A391: k <= len y by A386, NAT_1:13; then A392: k in dom y by A389, FINSEQ_3:25; then A393: (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k = y . k by FINSEQ_1:def_7 .= (b . k) * ((M * G) . k) by A181, A392 .= (b . k) * (M . (G . k)) by A180, A392, FUNCT_1:13 ; A394: k in Seg (len z) by A389, A390, FINSEQ_1:1; then A395: M . (H . k) = (M * H) . k by A343, A385, A386, FUNCT_1:13; H . k = G . k by A343, A385, A386, A391, A394; hence z . k = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k by A374, A386, A391, A393, A394, A395; ::_thesis: verum end; end; end; len (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) = (len y) + 1 by FINSEQ_2:16 .= len z by A374, FINSEQ_1:def_3 ; then A396: z = y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*> by A388, FINSEQ_1:14; len x = n + 1 by A7, A9, FINSEQ_3:29; then A397: x = x | (n + 1) by FINSEQ_1:58 .= x | (Seg (n + 1)) by FINSEQ_1:def_15 .= x1 ^ <*(x . (n + 1))*> by A7, A297, FINSEQ_5:10 .= x1 ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*> by A7, A8, A297 ; dom G <> {} proof assume dom G = {} ; ::_thesis: contradiction then {} = union (rng G) by RELAT_1:42, ZFMISC_1:2 .= dom (f | (union (rng (F | (Seg n))))) by A177, MESFUNC3:def_1 ; hence contradiction by A172; ::_thesis: verum end; then b <> {} by A177, MESFUNC3:def_1, RELAT_1:38; then len b in Seg (len b) by FINSEQ_1:3; then A398: 1 <= len b by FINSEQ_1:1; A399: for k being Nat st 1 <= k & k <= len H holds H . k = (G ^ <*(F . (n + 1))*>) . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len H implies H . k = (G ^ <*(F . (n + 1))*>) . k ) assume that A400: 1 <= k and A401: k <= len H ; ::_thesis: H . k = (G ^ <*(F . (n + 1))*>) . k k in Seg ((len G) + 1) by A370, A400, A401, FINSEQ_1:1; then A402: S3[k,H . k] by A343; percases ( k = (len G) + 1 or k <> (len G) + 1 ) ; suppose k = (len G) + 1 ; ::_thesis: H . k = (G ^ <*(F . (n + 1))*>) . k hence H . k = (G ^ <*(F . (n + 1))*>) . k by A402, FINSEQ_1:42; ::_thesis: verum end; suppose k <> (len G) + 1 ; ::_thesis: H . k = (G ^ <*(F . (n + 1))*>) . k then A403: k < (len G) + 1 by A369, A401, XXREAL_0:1; then k <= len G by NAT_1:13; then k in dom G by A400, FINSEQ_3:25; hence H . k = (G ^ <*(F . (n + 1))*>) . k by A402, A403, FINSEQ_1:def_7, NAT_1:13; ::_thesis: verum end; end; end; len H = (len G) + 1 by A343, FINSEQ_1:def_3 .= (len G) + (len <*(F . (n + 1))*>) by FINSEQ_1:39 .= len (G ^ <*(F . (n + 1))*>) by FINSEQ_1:22 ; then H = G ^ <*(F . (n + 1))*> by A399, FINSEQ_1:14; then A404: rng H = (rng G) \/ (rng <*(F . (n + 1))*>) by FINSEQ_1:31 .= (rng G) \/ {(F . (n + 1))} by FINSEQ_1:38 ; F | (Seg (n + 1)) = F1 ^ <*(F . (n + 1))*> by A174, FINSEQ_1:4, FINSEQ_5:10; then F1 ^ <*(F . (n + 1))*> = F | (n + 1) by FINSEQ_1:def_15 .= F by A9, FINSEQ_1:58 ; then rng F = (rng F1) \/ (rng <*(F . (n + 1))*>) by FINSEQ_1:31 .= (rng F1) \/ {(F . (n + 1))} by FINSEQ_1:38 ; then A405: dom f = union ((rng F1) \/ {(F . (n + 1))}) by A6, MESFUNC3:def_1 .= (dom (f | (union (rng (F | (Seg n)))))) \/ (union {(F . (n + 1))}) by A16, ZFMISC_1:78 .= (union (rng G)) \/ (union {(F . (n + 1))}) by A177, MESFUNC3:def_1 .= union (rng H) by A404, ZFMISC_1:78 ; for m being Nat st m in dom H holds for v being set st v in H . m holds f . v = c . m proof let m be Nat; ::_thesis: ( m in dom H implies for v being set st v in H . m holds f . v = c . m ) assume A406: m in dom H ; ::_thesis: for v being set st v in H . m holds f . v = c . m then A407: S3[m,H . m] by A343; A408: m <= (len G) + 1 by A343, A406, FINSEQ_1:1; let v be set ; ::_thesis: ( v in H . m implies f . v = c . m ) assume A409: v in H . m ; ::_thesis: f . v = c . m A410: S2[m,c . m] by A343, A296, A336, A406; A411: 1 <= m by A343, A406, FINSEQ_1:1; percases ( m = (len G) + 1 or m <> (len G) + 1 ) ; supposeA412: m = (len G) + 1 ; ::_thesis: f . v = c . m n + 1 in dom F by A174, FINSEQ_1:4; hence f . v = c . m by A6, A335, A407, A410, A409, A412, FINSEQ_1:6, MESFUNC3:def_1; ::_thesis: verum end; suppose m <> (len G) + 1 ; ::_thesis: f . v = c . m then A413: m < (len G) + 1 by A408, XXREAL_0:1; then A414: m <= len G by NAT_1:13; then m in Seg (len G) by A411, FINSEQ_1:1; then m in dom G by FINSEQ_1:def_3; then A415: G . m in rng G by FUNCT_1:3; H . m in rng H by A406, FUNCT_1:3; then A416: v in dom f by A405, A409, TARSKI:def_4; union (rng G) = union (rng F1) by A16, A177, MESFUNC3:def_1; then v in union (rng F1) by A407, A409, A413, A415, NAT_1:13, TARSKI:def_4; then v in (dom f) /\ (union (rng F1)) by A416, XBOOLE_0:def_4; then A417: v in dom (f | (union (rng (F | (Seg n))))) by RELAT_1:61; m in Seg (len G) by A411, A414, FINSEQ_1:1; then m in dom G by FINSEQ_1:def_3; then (f | (union (rng (F | (Seg n))))) . v = c . m by A177, A336, A407, A410, A409, A413, MESFUNC3:def_1, NAT_1:13; hence f . v = c . m by A417, FUNCT_1:47; ::_thesis: verum end; end; end; then A418: H,c are_Re-presentation_of f by A343, A296, A336, A405, MESFUNC3:def_1; 1 <= (len b) + 1 by NAT_1:11; then 1 in Seg ((len b) + 1) by FINSEQ_1:1; then c . 1 = 0. by A178, A296, A398; then integral (X,S,M,f) = Sum z by A3, A5, A343, A303, A374, A375, A380, A418, MESFUNC3:def_2 .= (Sum y) + (Sum <*((a . (n + 1)) * ((M * H) . (len z)))*>) by A379, A310, A396, EXTREAL1:10 .= (integral (X,S,M,(f | (union (rng (F | (Seg n))))))) + ((a . (n + 1)) * ((M * H) . (len z))) by A182, EXTREAL1:8 .= (Sum x1) + ((a . (n + 1)) * ((M * F) . (n + 1))) by A2, A23, A12, A28, A14, A172, A183, A176, A379 .= (Sum x1) + (Sum <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) by EXTREAL1:8 .= Sum x by A310, A324, A397, EXTREAL1:10 ; hence integral (X,S,M,f) = Sum x ; ::_thesis: verum end; end; end; hence integral (X,S,M,f) = Sum x ; ::_thesis: verum end; end; end; hence integral (X,S,M,f) = Sum x ; ::_thesis: verum end; A419: S1[ 0 ] proof let f be PartFunc of X,ExtREAL; ::_thesis: for F being Finite_Sep_Sequence of S for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds x . i = (a . i) * ((M * F) . i) ) & len F = 0 holds integral (X,S,M,f) = Sum x let F be Finite_Sep_Sequence of S; ::_thesis: for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds x . i = (a . i) * ((M * F) . i) ) & len F = 0 holds integral (X,S,M,f) = Sum x let a, x be FinSequence of ExtREAL ; ::_thesis: ( f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds x . i = (a . i) * ((M * F) . i) ) & len F = 0 implies integral (X,S,M,f) = Sum x ) assume that f is_simple_func_in S and A420: dom f <> {} and for x being set st x in dom f holds 0. <= f . x and A421: F,a are_Re-presentation_of f and dom x = dom F and for i being Nat st i in dom x holds x . i = (a . i) * ((M * F) . i) and A422: len F = 0 ; ::_thesis: integral (X,S,M,f) = Sum x Seg (len F) = {} by A422; then dom F = {} by FINSEQ_1:def_3; then union (rng F) = {} by RELAT_1:42, ZFMISC_1:2; hence integral (X,S,M,f) = Sum x by A420, A421, MESFUNC3:def_1; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A419, A1); hence for n being Nat for f being PartFunc of X,ExtREAL for F being Finite_Sep_Sequence of S for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for i being Nat st i in dom x holds x . i = (a . i) * ((M * F) . i) ) & len F = n holds integral (X,S,M,f) = Sum x ; ::_thesis: verum end; theorem Th3: :: MESFUNC4:3 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for M being sigma_Measure of S for F being Finite_Sep_Sequence of S for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) holds integral (X,S,M,f) = Sum x proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for M being sigma_Measure of S for F being Finite_Sep_Sequence of S for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) holds integral (X,S,M,f) = Sum x let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for M being sigma_Measure of S for F being Finite_Sep_Sequence of S for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) holds integral (X,S,M,f) = Sum x let f be PartFunc of X,ExtREAL; ::_thesis: for M being sigma_Measure of S for F being Finite_Sep_Sequence of S for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) holds integral (X,S,M,f) = Sum x let M be sigma_Measure of S; ::_thesis: for F being Finite_Sep_Sequence of S for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) holds integral (X,S,M,f) = Sum x let F be Finite_Sep_Sequence of S; ::_thesis: for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) holds integral (X,S,M,f) = Sum x let a, x be FinSequence of ExtREAL ; ::_thesis: ( f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) implies integral (X,S,M,f) = Sum x ) A1: len F = len F ; assume ( f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) ) ; ::_thesis: integral (X,S,M,f) = Sum x hence integral (X,S,M,f) = Sum x by A1, Th2; ::_thesis: verum end; theorem Th4: :: MESFUNC4:4 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for M being sigma_Measure of S st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) holds ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & integral (X,S,M,f) = Sum x ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for M being sigma_Measure of S st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) holds ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & integral (X,S,M,f) = Sum x ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for M being sigma_Measure of S st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) holds ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & integral (X,S,M,f) = Sum x ) let f be PartFunc of X,ExtREAL; ::_thesis: for M being sigma_Measure of S st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) holds ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & integral (X,S,M,f) = Sum x ) let M be sigma_Measure of S; ::_thesis: ( f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) implies ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & integral (X,S,M,f) = Sum x ) ) assume that A1: f is_simple_func_in S and A2: ( dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) ) ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & integral (X,S,M,f) = Sum x ) consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that A3: F,a are_Re-presentation_of f by A1, MESFUNC3:12; ex x being FinSequence of ExtREAL st ( dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) ) proof deffunc H1( Nat) -> Element of ExtREAL = (a . $1) * ((M * F) . $1); consider x being FinSequence of ExtREAL such that A4: ( len x = len F & ( for k being Nat st k in dom x holds x . k = H1(k) ) ) from FINSEQ_2:sch_1(); take x ; ::_thesis: ( dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) ) dom x = Seg (len F) by A4, FINSEQ_1:def_3 .= dom F by FINSEQ_1:def_3 ; hence ( dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) ) by A4; ::_thesis: verum end; then consider x being FinSequence of ExtREAL such that A5: ( dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) ) ; integral (X,S,M,f) = Sum x by A1, A2, A3, A5, Th3; hence ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st ( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) ) & integral (X,S,M,f) = Sum x ) by A3, A5; ::_thesis: verum end; theorem :: MESFUNC4:5 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & g is_simple_func_in S & dom g = dom f & ( for x being set st x in dom g holds 0. <= g . x ) holds ( f + g is_simple_func_in S & dom (f + g) <> {} & ( for x being set st x in dom (f + g) holds 0. <= (f + g) . x ) & integral (X,S,M,(f + g)) = (integral (X,S,M,f)) + (integral (X,S,M,g)) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & g is_simple_func_in S & dom g = dom f & ( for x being set st x in dom g holds 0. <= g . x ) holds ( f + g is_simple_func_in S & dom (f + g) <> {} & ( for x being set st x in dom (f + g) holds 0. <= (f + g) . x ) & integral (X,S,M,(f + g)) = (integral (X,S,M,f)) + (integral (X,S,M,g)) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & g is_simple_func_in S & dom g = dom f & ( for x being set st x in dom g holds 0. <= g . x ) holds ( f + g is_simple_func_in S & dom (f + g) <> {} & ( for x being set st x in dom (f + g) holds 0. <= (f + g) . x ) & integral (X,S,M,(f + g)) = (integral (X,S,M,f)) + (integral (X,S,M,g)) ) let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & g is_simple_func_in S & dom g = dom f & ( for x being set st x in dom g holds 0. <= g . x ) holds ( f + g is_simple_func_in S & dom (f + g) <> {} & ( for x being set st x in dom (f + g) holds 0. <= (f + g) . x ) & integral (X,S,M,(f + g)) = (integral (X,S,M,f)) + (integral (X,S,M,g)) ) let f, g be PartFunc of X,ExtREAL; ::_thesis: ( f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & g is_simple_func_in S & dom g = dom f & ( for x being set st x in dom g holds 0. <= g . x ) implies ( f + g is_simple_func_in S & dom (f + g) <> {} & ( for x being set st x in dom (f + g) holds 0. <= (f + g) . x ) & integral (X,S,M,(f + g)) = (integral (X,S,M,f)) + (integral (X,S,M,g)) ) ) assume that A1: f is_simple_func_in S and A2: dom f <> {} and A3: for x being set st x in dom f holds 0. <= f . x and A4: g is_simple_func_in S and A5: dom g = dom f and A6: for x being set st x in dom g holds 0. <= g . x ; ::_thesis: ( f + g is_simple_func_in S & dom (f + g) <> {} & ( for x being set st x in dom (f + g) holds 0. <= (f + g) . x ) & integral (X,S,M,(f + g)) = (integral (X,S,M,f)) + (integral (X,S,M,g)) ) A7: g is V63() by A4, MESFUNC2:def_4; then A8: dom (f + g) = (dom f) /\ (dom f) by A5, MESFUNC2:2 .= dom f ; consider G being Finite_Sep_Sequence of S, b, y being FinSequence of ExtREAL such that A9: G,b are_Re-presentation_of g and dom y = dom G and for n being Nat st n in dom y holds y . n = (b . n) * ((M * G) . n) and integral (X,S,M,g) = Sum y by A2, A4, A5, A6, Th4; set lb = len b; consider F being Finite_Sep_Sequence of S, a, x being FinSequence of ExtREAL such that A10: F,a are_Re-presentation_of f and dom x = dom F and for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) and integral (X,S,M,f) = Sum x by A1, A2, A3, Th4; deffunc H1( Nat) -> Element of ExtREAL = b . ((($1 -' 1) mod (len b)) + 1); deffunc H2( Nat) -> Element of ExtREAL = a . ((($1 -' 1) div (len b)) + 1); set la = len a; A11: dom F = dom a by A10, MESFUNC3:def_1; deffunc H3( Nat) -> set = (F . ((($1 -' 1) div (len b)) + 1)) /\ (G . ((($1 -' 1) mod (len b)) + 1)); consider FG being FinSequence such that A12: len FG = (len a) * (len b) and A13: for k being Nat st k in dom FG holds FG . k = H3(k) from FINSEQ_1:sch_2(); A14: dom FG = Seg ((len a) * (len b)) by A12, FINSEQ_1:def_3; A15: dom G = dom b by A9, MESFUNC3:def_1; now__::_thesis:_for_k_being_Nat_st_k_in_dom_FG_holds_ FG_._k_in_S reconsider la9 = len a, lb9 = len b as Nat ; let k be Nat; ::_thesis: ( k in dom FG implies FG . k in S ) set i = ((k -' 1) div (len b)) + 1; set j = ((k -' 1) mod (len b)) + 1; assume A16: k in dom FG ; ::_thesis: FG . k in S then A17: k in Seg ((len a) * (len b)) by A12, FINSEQ_1:def_3; then A18: k <= (len a) * (len b) by FINSEQ_1:1; then k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42; then A19: (k -' 1) div (len b) <= (((len a) * (len b)) -' 1) div (len b) by NAT_2:24; 1 <= k by A17, FINSEQ_1:1; then A20: ( lb9 divides la9 * lb9 & 1 <= (len a) * (len b) ) by A18, NAT_D:def_3, XXREAL_0:2; A21: len b <> 0 by A17; then len b >= 0 + 1 by NAT_1:13; then ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A20, NAT_2:15; then A22: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by A19, XREAL_1:19; reconsider la = len a, lb = len b as Nat ; ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) div (len b)) + 1 <= la ) by A21, A22, NAT_D:18, XREAL_1:6; then ((k -' 1) div (len b)) + 1 in Seg la by FINSEQ_1:1; then ((k -' 1) div (len b)) + 1 in dom F by A11, FINSEQ_1:def_3; then A23: F . (((k -' 1) div (len b)) + 1) in rng F by FUNCT_1:3; (k -' 1) mod lb < lb by A21, NAT_D:1; then ( ((k -' 1) mod (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 <= lb ) by NAT_1:13; then ((k -' 1) mod (len b)) + 1 in Seg lb by FINSEQ_1:1; then ((k -' 1) mod (len b)) + 1 in dom G by A15, FINSEQ_1:def_3; then A24: G . (((k -' 1) mod (len b)) + 1) in rng G by FUNCT_1:3; ( rng F c= S & rng G c= S ) by FINSEQ_1:def_4; then (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) in S by A23, A24, MEASURE1:34; hence FG . k in S by A13, A16; ::_thesis: verum end; then reconsider FG = FG as FinSequence of S by FINSEQ_2:12; for k, l being Nat st k in dom FG & l in dom FG & k <> l holds FG . k misses FG . l proof reconsider la9 = len a, lb9 = len b as Nat ; let k, l be Nat; ::_thesis: ( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l ) assume that A25: k in dom FG and A26: l in dom FG and A27: k <> l ; ::_thesis: FG . k misses FG . l A28: l in Seg ((len a) * (len b)) by A12, A26, FINSEQ_1:def_3; set m = ((l -' 1) mod (len b)) + 1; set n = ((l -' 1) div (len b)) + 1; set j = ((k -' 1) mod (len b)) + 1; set i = ((k -' 1) div (len b)) + 1; A29: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A25; A30: k in Seg ((len a) * (len b)) by A12, A25, FINSEQ_1:def_3; then A31: k <= (len a) * (len b) by FINSEQ_1:1; A32: 1 <= k by A30, FINSEQ_1:1; then A33: ( lb9 divides la9 * lb9 & 1 <= (len a) * (len b) ) by A31, NAT_D:def_3, XXREAL_0:2; A34: len b <> 0 by A30; then len b >= 0 + 1 by NAT_1:13; then A35: ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A33, NAT_2:15; k -' 1 <= ((len a) * (len b)) -' 1 by A31, NAT_D:42; then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A35, NAT_2:24; then A36: ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19; reconsider la = len a, lb = len b as Nat ; ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) div (len b)) + 1 <= la ) by A34, A36, NAT_D:18, XREAL_1:6; then ((k -' 1) div (len b)) + 1 in Seg la by FINSEQ_1:1; then A37: ((k -' 1) div (len b)) + 1 in dom F by A11, FINSEQ_1:def_3; A38: 1 <= l by A28, FINSEQ_1:1; A39: ( ((k -' 1) div (len b)) + 1 <> ((l -' 1) div (len b)) + 1 or ((k -' 1) mod (len b)) + 1 <> ((l -' 1) mod (len b)) + 1 ) proof (l -' 1) + 1 = ((((((l -' 1) div (len b)) + 1) - 1) * lb) + ((((l -' 1) mod (len b)) + 1) - 1)) + 1 by A34, NAT_D:2; then A40: (l - 1) + 1 = (((((l -' 1) div (len b)) + 1) - 1) * lb) + (((l -' 1) mod (len b)) + 1) by A38, XREAL_1:233; (k -' 1) + 1 = ((((((k -' 1) div (len b)) + 1) - 1) * lb) + ((((k -' 1) mod (len b)) + 1) - 1)) + 1 by A34, NAT_D:2; then A41: (k - 1) + 1 = (((((k -' 1) div (len b)) + 1) - 1) * lb) + (((k -' 1) mod (len b)) + 1) by A32, XREAL_1:233; assume ( ((k -' 1) div (len b)) + 1 = ((l -' 1) div (len b)) + 1 & ((k -' 1) mod (len b)) + 1 = ((l -' 1) mod (len b)) + 1 ) ; ::_thesis: contradiction hence contradiction by A27, A41, A40; ::_thesis: verum end; (l -' 1) mod lb < lb by A34, NAT_D:1; then ( ((l -' 1) mod (len b)) + 1 >= 0 + 1 & ((l -' 1) mod (len b)) + 1 <= lb ) by NAT_1:13; then ((l -' 1) mod (len b)) + 1 in Seg lb by FINSEQ_1:1; then A42: ((l -' 1) mod (len b)) + 1 in dom G by A15, FINSEQ_1:def_3; (k -' 1) mod lb < lb by A34, NAT_D:1; then ( ((k -' 1) mod (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 <= lb ) by NAT_1:13; then ((k -' 1) mod (len b)) + 1 in Seg lb by FINSEQ_1:1; then A43: ((k -' 1) mod (len b)) + 1 in dom G by A15, FINSEQ_1:def_3; l <= la * lb by A28, FINSEQ_1:1; then l -' 1 <= (la * lb) -' 1 by NAT_D:42; then (l -' 1) div lb <= ((la * lb) div lb) - 1 by A35, NAT_2:24; then ((l -' 1) div lb) + 1 <= (la * lb) div lb by XREAL_1:19; then ( ((l -' 1) div (len b)) + 1 >= 0 + 1 & ((l -' 1) div (len b)) + 1 <= la ) by A34, NAT_D:18, XREAL_1:6; then ((l -' 1) div (len b)) + 1 in Seg la by FINSEQ_1:1; then A44: ((l -' 1) div (len b)) + 1 in dom F by A11, FINSEQ_1:def_3; percases ( ((k -' 1) div (len b)) + 1 <> ((l -' 1) div (len b)) + 1 or ((k -' 1) mod (len b)) + 1 <> ((l -' 1) mod (len b)) + 1 ) by A39; suppose ((k -' 1) div (len b)) + 1 <> ((l -' 1) div (len b)) + 1 ; ::_thesis: FG . k misses FG . l then A45: F . (((k -' 1) div (len b)) + 1) misses F . (((l -' 1) div (len b)) + 1) by A37, A44, MESFUNC3:4; (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by A13, A26, A29 .= (F . (((k -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16 .= (F . (((k -' 1) div (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16 .= ((F . (((k -' 1) div (len b)) + 1)) /\ (F . (((l -' 1) div (len b)) + 1))) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by XBOOLE_1:16 .= {} /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by A45, XBOOLE_0:def_7 .= {} ; hence FG . k misses FG . l by XBOOLE_0:def_7; ::_thesis: verum end; suppose ((k -' 1) mod (len b)) + 1 <> ((l -' 1) mod (len b)) + 1 ; ::_thesis: FG . k misses FG . l then A46: G . (((k -' 1) mod (len b)) + 1) misses G . (((l -' 1) mod (len b)) + 1) by A43, A42, MESFUNC3:4; (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by A13, A26, A29 .= (F . (((k -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16 .= (F . (((k -' 1) div (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16 .= ((F . (((k -' 1) div (len b)) + 1)) /\ (F . (((l -' 1) div (len b)) + 1))) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by XBOOLE_1:16 .= ((F . (((k -' 1) div (len b)) + 1)) /\ (F . (((l -' 1) div (len b)) + 1))) /\ {} by A46, XBOOLE_0:def_7 .= {} ; hence FG . k misses FG . l by XBOOLE_0:def_7; ::_thesis: verum end; end; end; then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4; consider a1 being FinSequence of ExtREAL such that A47: len a1 = len FG and A48: for k being Nat st k in dom a1 holds a1 . k = H2(k) from FINSEQ_2:sch_1(); consider b1 being FinSequence of ExtREAL such that A49: len b1 = len FG and A50: for k being Nat st k in dom b1 holds b1 . k = H1(k) from FINSEQ_2:sch_1(); A51: dom f = union (rng F) by A10, MESFUNC3:def_1; A52: dom a1 = Seg (len FG) by A47, FINSEQ_1:def_3; A53: for k being Nat st k in dom FG holds for x being set st x in FG . k holds f . x = a1 . k proof reconsider la9 = len a, lb9 = len b as Nat ; let k be Nat; ::_thesis: ( k in dom FG implies for x being set st x in FG . k holds f . x = a1 . k ) set i = ((k -' 1) div (len b)) + 1; assume A54: k in dom FG ; ::_thesis: for x being set st x in FG . k holds f . x = a1 . k then A55: k in Seg (len FG) by FINSEQ_1:def_3; A56: k in Seg (len FG) by A54, FINSEQ_1:def_3; then A57: k <= (len a) * (len b) by A12, FINSEQ_1:1; A58: len b <> 0 by A12, A56; then A59: len b >= 0 + 1 by NAT_1:13; 1 <= k by A56, FINSEQ_1:1; then ( lb9 divides la9 * lb9 & 1 <= (len a) * (len b) ) by A57, NAT_D:def_3, XXREAL_0:2; then A60: ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A59, NAT_2:15; A61: ((len a) * (len b)) div (len b) = len a by A58, NAT_D:18; k -' 1 <= ((len a) * (len b)) -' 1 by A57, NAT_D:42; then (k -' 1) div (len b) <= (((len a) * (len b)) -' 1) div (len b) by NAT_2:24; then ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) ) by A60, XREAL_1:6, XREAL_1:19; then ((k -' 1) div (len b)) + 1 in Seg (len a) by A61, FINSEQ_1:1; then A62: ((k -' 1) div (len b)) + 1 in dom F by A11, FINSEQ_1:def_3; let x be set ; ::_thesis: ( x in FG . k implies f . x = a1 . k ) assume A63: x in FG . k ; ::_thesis: f . x = a1 . k FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A54; then x in F . (((k -' 1) div (len b)) + 1) by A63, XBOOLE_0:def_4; hence f . x = a . (((k -' 1) div (len b)) + 1) by A10, A62, MESFUNC3:def_1 .= a1 . k by A48, A52, A55 ; ::_thesis: verum end; A64: dom b1 = Seg (len FG) by A49, FINSEQ_1:def_3; A65: for k being Nat st k in dom FG holds for x being set st x in FG . k holds g . x = b1 . k proof let k be Nat; ::_thesis: ( k in dom FG implies for x being set st x in FG . k holds g . x = b1 . k ) set j = ((k -' 1) mod (len b)) + 1; assume A66: k in dom FG ; ::_thesis: for x being set st x in FG . k holds g . x = b1 . k then A67: k in Seg (len FG) by FINSEQ_1:def_3; k in Seg (len FG) by A66, FINSEQ_1:def_3; then len b <> 0 by A12; then (k -' 1) mod (len b) < len b by NAT_D:1; then ( ((k -' 1) mod (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 <= len b ) by NAT_1:13; then ((k -' 1) mod (len b)) + 1 in Seg (len b) by FINSEQ_1:1; then A68: ((k -' 1) mod (len b)) + 1 in dom G by A15, FINSEQ_1:def_3; let x be set ; ::_thesis: ( x in FG . k implies g . x = b1 . k ) assume A69: x in FG . k ; ::_thesis: g . x = b1 . k FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A66; then x in G . (((k -' 1) mod (len b)) + 1) by A69, XBOOLE_0:def_4; hence g . x = b . (((k -' 1) mod (len b)) + 1) by A9, A68, MESFUNC3:def_1 .= b1 . k by A50, A64, A67 ; ::_thesis: verum end; A70: dom g = union (rng G) by A9, MESFUNC3:def_1; A71: dom f = union (rng FG) proof thus dom f c= union (rng FG) :: according to XBOOLE_0:def_10 ::_thesis: union (rng FG) c= dom f proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom f or z in union (rng FG) ) assume A72: z in dom f ; ::_thesis: z in union (rng FG) then consider Y being set such that A73: z in Y and A74: Y in rng F by A51, TARSKI:def_4; consider Z being set such that A75: z in Z and A76: Z in rng G by A5, A70, A72, TARSKI:def_4; consider j being set such that A77: j in dom G and A78: Z = G . j by A76, FUNCT_1:def_3; reconsider j = j as Element of NAT by A77; A79: j in Seg (len b) by A15, A77, FINSEQ_1:def_3; then A80: 1 <= j by FINSEQ_1:1; then consider j9 being Nat such that A81: j = 1 + j9 by NAT_1:10; consider i being set such that A82: i in dom F and A83: Y = F . i by A74, FUNCT_1:def_3; reconsider i = i as Element of NAT by A82; A84: i in Seg (len a) by A11, A82, FINSEQ_1:def_3; then 1 <= i by FINSEQ_1:1; then consider i9 being Nat such that A85: i = 1 + i9 by NAT_1:10; A86: j <= len b by A79, FINSEQ_1:1; then A87: j9 < len b by A81, NAT_1:13; set k = ((i - 1) * (len b)) + j; reconsider k = ((i - 1) * (len b)) + j as Nat by A85; A88: k >= 0 + j by A85, XREAL_1:6; then A89: k -' 1 = k - 1 by A80, XREAL_1:233, XXREAL_0:2 .= (i9 * (len b)) + j9 by A85, A81 ; then A90: i = ((k -' 1) div (len b)) + 1 by A85, A87, NAT_D:def_1; i <= len a by A84, FINSEQ_1:1; then i - 1 <= (len a) - 1 by XREAL_1:9; then (i - 1) * (len b) <= ((len a) - 1) * (len b) by XREAL_1:64; then A91: k <= (((len a) - 1) * (len b)) + j by XREAL_1:6; (((len a) - 1) * (len b)) + j <= (((len a) - 1) * (len b)) + (len b) by A86, XREAL_1:6; then A92: k <= (len a) * (len b) by A91, XXREAL_0:2; k >= 1 by A80, A88, XXREAL_0:2; then A93: k in Seg ((len a) * (len b)) by A92, FINSEQ_1:1; then k in dom FG by A12, FINSEQ_1:def_3; then A94: FG . k in rng FG by FUNCT_1:def_3; A95: j = ((k -' 1) mod (len b)) + 1 by A81, A89, A87, NAT_D:def_2; z in (F . i) /\ (G . j) by A73, A83, A75, A78, XBOOLE_0:def_4; then z in FG . k by A13, A14, A90, A95, A93; hence z in union (rng FG) by A94, TARSKI:def_4; ::_thesis: verum end; reconsider la9 = len a, lb9 = len b as Nat ; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union (rng FG) or z in dom f ) assume z in union (rng FG) ; ::_thesis: z in dom f then consider Y being set such that A96: z in Y and A97: Y in rng FG by TARSKI:def_4; consider k being set such that A98: k in dom FG and A99: Y = FG . k by A97, FUNCT_1:def_3; reconsider k = k as Element of NAT by A98; set j = ((k -' 1) mod (len b)) + 1; set i = ((k -' 1) div (len b)) + 1; FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A98; then A100: z in F . (((k -' 1) div (len b)) + 1) by A96, A99, XBOOLE_0:def_4; A101: k in Seg (len FG) by A98, FINSEQ_1:def_3; then A102: k <= (len a) * (len b) by A12, FINSEQ_1:1; A103: len b <> 0 by A12, A101; then A104: len b >= 0 + 1 by NAT_1:13; 1 <= k by A101, FINSEQ_1:1; then ( lb9 divides la9 * lb9 & 1 <= (len a) * (len b) ) by A102, NAT_D:def_3, XXREAL_0:2; then A105: ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A104, NAT_2:15; reconsider i = ((k -' 1) div (len b)) + 1 as Nat ; A106: ((len a) * (len b)) div (len b) = len a by A103, NAT_D:18; k -' 1 <= ((len a) * (len b)) -' 1 by A102, NAT_D:42; then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A105, NAT_2:24; then ( i >= 0 + 1 & i <= ((len a) * (len b)) div (len b) ) by XREAL_1:6, XREAL_1:19; then i in Seg (len a) by A106, FINSEQ_1:1; then i in dom F by A11, FINSEQ_1:def_3; then F . i in rng F by FUNCT_1:def_3; hence z in dom f by A51, A100, TARSKI:def_4; ::_thesis: verum end; A107: for k being Nat for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds (f + g) . x = (f + g) . y proof reconsider la9 = len a, lb9 = len b as Nat ; let k be Nat; ::_thesis: for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds (f + g) . x = (f + g) . y let x, y be Element of X; ::_thesis: ( k in dom FG & x in FG . k & y in FG . k implies (f + g) . x = (f + g) . y ) assume that A108: k in dom FG and A109: x in FG . k and A110: y in FG . k ; ::_thesis: (f + g) . x = (f + g) . y set j = ((k -' 1) mod (len b)) + 1; A111: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A108; then A112: x in G . (((k -' 1) mod (len b)) + 1) by A109, XBOOLE_0:def_4; set i = ((k -' 1) div (len b)) + 1; A113: k in Seg (len FG) by A108, FINSEQ_1:def_3; then A114: k <= (len a) * (len b) by A12, FINSEQ_1:1; then A115: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42; 1 <= k by A113, FINSEQ_1:1; then A116: ( lb9 divides la9 * lb9 & 1 <= (len a) * (len b) ) by A114, NAT_D:def_3, XXREAL_0:2; A117: len b <> 0 by A12, A113; then len b >= 0 + 1 by NAT_1:13; then ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A116, NAT_2:15; then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A115, NAT_2:24; then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19; then ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) div (len b)) + 1 <= len a ) by A117, NAT_D:18, XREAL_1:6; then ((k -' 1) div (len b)) + 1 in Seg (len a) by FINSEQ_1:1; then A118: ((k -' 1) div (len b)) + 1 in dom F by A11, FINSEQ_1:def_3; x in F . (((k -' 1) div (len b)) + 1) by A109, A111, XBOOLE_0:def_4; then A119: f . x = a . (((k -' 1) div (len b)) + 1) by A10, A118, MESFUNC3:def_1; (k -' 1) mod (len b) < len b by A117, NAT_D:1; then ( ((k -' 1) mod (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 <= len b ) by NAT_1:13; then ((k -' 1) mod (len b)) + 1 in Seg (len b) by FINSEQ_1:1; then A120: ((k -' 1) mod (len b)) + 1 in dom G by A15, FINSEQ_1:def_3; y in F . (((k -' 1) div (len b)) + 1) by A110, A111, XBOOLE_0:def_4; then A121: f . y = a . (((k -' 1) div (len b)) + 1) by A10, A118, MESFUNC3:def_1; A122: y in G . (((k -' 1) mod (len b)) + 1) by A110, A111, XBOOLE_0:def_4; A123: FG . k in rng FG by A108, FUNCT_1:def_3; then A124: y in dom (f + g) by A71, A8, A110, TARSKI:def_4; x in dom (f + g) by A71, A8, A109, A123, TARSKI:def_4; hence (f + g) . x = (f . x) + (g . x) by MESFUNC1:def_3 .= (a . (((k -' 1) div (len b)) + 1)) + (b . (((k -' 1) mod (len b)) + 1)) by A9, A120, A112, A119, MESFUNC3:def_1 .= (f . y) + (g . y) by A9, A120, A122, A121, MESFUNC3:def_1 .= (f + g) . y by A124, MESFUNC1:def_3 ; ::_thesis: verum end; ex y1 being FinSequence of ExtREAL st ( dom y1 = dom FG & ( for n being Nat st n in dom y1 holds y1 . n = (b1 . n) * ((M * FG) . n) ) ) proof deffunc H4( Nat) -> Element of ExtREAL = (b1 . $1) * ((M * FG) . $1); consider y1 being FinSequence of ExtREAL such that A125: ( len y1 = len FG & ( for k being Nat st k in dom y1 holds y1 . k = H4(k) ) ) from FINSEQ_2:sch_1(); take y1 ; ::_thesis: ( dom y1 = dom FG & ( for n being Nat st n in dom y1 holds y1 . n = (b1 . n) * ((M * FG) . n) ) ) dom y1 = Seg (len FG) by A125, FINSEQ_1:def_3 .= dom FG by FINSEQ_1:def_3 ; hence ( dom y1 = dom FG & ( for n being Nat st n in dom y1 holds y1 . n = (b1 . n) * ((M * FG) . n) ) ) by A125; ::_thesis: verum end; then consider y1 being FinSequence of ExtREAL such that A126: dom y1 = dom FG and A127: for n being Nat st n in dom y1 holds y1 . n = (b1 . n) * ((M * FG) . n) ; ex x1 being FinSequence of ExtREAL st ( dom x1 = dom FG & ( for n being Nat st n in dom x1 holds x1 . n = (a1 . n) * ((M * FG) . n) ) ) proof deffunc H4( Nat) -> Element of ExtREAL = (a1 . $1) * ((M * FG) . $1); consider x1 being FinSequence of ExtREAL such that A128: ( len x1 = len FG & ( for k being Nat st k in dom x1 holds x1 . k = H4(k) ) ) from FINSEQ_2:sch_1(); take x1 ; ::_thesis: ( dom x1 = dom FG & ( for n being Nat st n in dom x1 holds x1 . n = (a1 . n) * ((M * FG) . n) ) ) thus ( dom x1 = dom FG & ( for n being Nat st n in dom x1 holds x1 . n = (a1 . n) * ((M * FG) . n) ) ) by A128, FINSEQ_3:29; ::_thesis: verum end; then consider x1 being FinSequence of ExtREAL such that A129: dom x1 = dom FG and A130: for n being Nat st n in dom x1 holds x1 . n = (a1 . n) * ((M * FG) . n) ; dom FG = Seg (len a1) by A47, FINSEQ_1:def_3 .= dom a1 by FINSEQ_1:def_3 ; then FG,a1 are_Re-presentation_of f by A71, A53, MESFUNC3:def_1; then A131: integral (X,S,M,f) = Sum x1 by A1, A2, A3, A129, A130, Th3; deffunc H4( Nat) -> Element of ExtREAL = (a1 . $1) + (b1 . $1); consider c1 being FinSequence of ExtREAL such that A132: len c1 = len FG and A133: for k being Nat st k in dom c1 holds c1 . k = H4(k) from FINSEQ_2:sch_1(); ex z1 being FinSequence of ExtREAL st ( dom z1 = dom FG & ( for n being Nat st n in dom z1 holds z1 . n = (c1 . n) * ((M * FG) . n) ) ) proof deffunc H5( Nat) -> Element of ExtREAL = (c1 . $1) * ((M * FG) . $1); consider z1 being FinSequence of ExtREAL such that A134: ( len z1 = len FG & ( for k being Nat st k in dom z1 holds z1 . k = H5(k) ) ) from FINSEQ_2:sch_1(); take z1 ; ::_thesis: ( dom z1 = dom FG & ( for n being Nat st n in dom z1 holds z1 . n = (c1 . n) * ((M * FG) . n) ) ) thus ( dom z1 = dom FG & ( for n being Nat st n in dom z1 holds z1 . n = (c1 . n) * ((M * FG) . n) ) ) by A134, FINSEQ_3:29; ::_thesis: verum end; then consider z1 being FinSequence of ExtREAL such that A135: dom z1 = dom FG and A136: for n being Nat st n in dom z1 holds z1 . n = (c1 . n) * ((M * FG) . n) ; A137: dom c1 = Seg (len FG) by A132, FINSEQ_1:def_3; A138: for k being Nat st k in dom FG holds for x being set st x in FG . k holds (f + g) . x = c1 . k proof let k be Nat; ::_thesis: ( k in dom FG implies for x being set st x in FG . k holds (f + g) . x = c1 . k ) A139: dom (f + g) c= X by RELAT_1:def_18; assume A140: k in dom FG ; ::_thesis: for x being set st x in FG . k holds (f + g) . x = c1 . k then A141: k in Seg (len FG) by FINSEQ_1:def_3; let x be set ; ::_thesis: ( x in FG . k implies (f + g) . x = c1 . k ) assume A142: x in FG . k ; ::_thesis: (f + g) . x = c1 . k FG . k in rng FG by A140, FUNCT_1:def_3; then x in dom (f + g) by A71, A8, A142, TARSKI:def_4; hence (f + g) . x = (f . x) + (g . x) by A139, MESFUNC1:def_3 .= (a1 . k) + (g . x) by A53, A140, A142 .= (a1 . k) + (b1 . k) by A65, A140, A142 .= c1 . k by A133, A137, A141 ; ::_thesis: verum end; A143: for i being Nat st i in dom y1 holds 0. <= y1 . i proof let i be Nat; ::_thesis: ( i in dom y1 implies 0. <= y1 . i ) set i9 = ((i -' 1) mod (len b)) + 1; assume A144: i in dom y1 ; ::_thesis: 0. <= y1 . i then A145: y1 . i = (b1 . i) * ((M * FG) . i) by A127; A146: i in Seg (len FG) by A126, A144, FINSEQ_1:def_3; then len b <> 0 by A12; then (i -' 1) mod (len b) < len b by NAT_D:1; then ( ((i -' 1) mod (len b)) + 1 >= 0 + 1 & ((i -' 1) mod (len b)) + 1 <= len b ) by NAT_1:13; then ((i -' 1) mod (len b)) + 1 in Seg (len b) by FINSEQ_1:1; then A147: ((i -' 1) mod (len b)) + 1 in dom G by A15, FINSEQ_1:def_3; percases ( G . (((i -' 1) mod (len b)) + 1) <> {} or G . (((i -' 1) mod (len b)) + 1) = {} ) ; suppose G . (((i -' 1) mod (len b)) + 1) <> {} ; ::_thesis: 0. <= y1 . i then consider x9 being set such that A148: x9 in G . (((i -' 1) mod (len b)) + 1) by XBOOLE_0:def_1; ( FG . i in rng FG & rng FG c= S ) by A126, A144, FINSEQ_1:def_4, FUNCT_1:3; then reconsider FGi = FG . i as Element of S ; reconsider EMPTY = {} as Element of S by MEASURE1:7; EMPTY c= FGi by XBOOLE_1:2; then A149: M . {} <= M . FGi by MEASURE1:31; A150: G . (((i -' 1) mod (len b)) + 1) c= dom g by A70, A147, FUNCT_1:3, ZFMISC_1:74; g . x9 = b . (((i -' 1) mod (len b)) + 1) by A9, A147, A148, MESFUNC3:def_1 .= b1 . i by A50, A64, A146 ; then A151: 0. <= b1 . i by A6, A148, A150; M . {} = 0. by VALUED_0:def_19; then 0. <= (M * FG) . i by A126, A144, A149, FUNCT_1:13; hence 0. <= y1 . i by A145, A151; ::_thesis: verum end; supposeA152: G . (((i -' 1) mod (len b)) + 1) = {} ; ::_thesis: 0. <= y1 . i FG . i = (F . (((i -' 1) div (len b)) + 1)) /\ (G . (((i -' 1) mod (len b)) + 1)) by A13, A126, A144; then M . (FG . i) = 0. by A152, VALUED_0:def_19; then (M * FG) . i = 0. by A126, A144, FUNCT_1:13; hence 0. <= y1 . i by A145; ::_thesis: verum end; end; end; not -infty in rng y1 proof assume -infty in rng y1 ; ::_thesis: contradiction then ex i being set st ( i in dom y1 & y1 . i = -infty ) by FUNCT_1:def_3; hence contradiction by A143; ::_thesis: verum end; then A153: (x1 " {+infty}) /\ (y1 " {-infty}) = (x1 " {+infty}) /\ {} by FUNCT_1:72 .= {} ; A154: for i being Nat st i in dom x1 holds 0. <= x1 . i proof reconsider la9 = len a, lb9 = len b as Nat ; let i be Nat; ::_thesis: ( i in dom x1 implies 0. <= x1 . i ) set i9 = ((i -' 1) div (len b)) + 1; assume A155: i in dom x1 ; ::_thesis: 0. <= x1 . i then A156: x1 . i = (a1 . i) * ((M * FG) . i) by A130; A157: i in Seg (len FG) by A129, A155, FINSEQ_1:def_3; then A158: i <= (len a) * (len b) by A12, FINSEQ_1:1; A159: len b <> 0 by A12, A157; then A160: len b >= 0 + 1 by NAT_1:13; 1 <= i by A157, FINSEQ_1:1; then ( lb9 divides la9 * lb9 & 1 <= (len a) * (len b) ) by A158, NAT_D:def_3, XXREAL_0:2; then A161: ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A160, NAT_2:15; i -' 1 <= ((len a) * (len b)) -' 1 by A158, NAT_D:42; then (i -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A161, NAT_2:24; then A162: ( ((i -' 1) div (len b)) + 1 >= 0 + 1 & ((i -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) ) by XREAL_1:6, XREAL_1:19; ((len a) * (len b)) div (len b) = len a by A159, NAT_D:18; then ((i -' 1) div (len b)) + 1 in Seg (len a) by A162, FINSEQ_1:1; then A163: ((i -' 1) div (len b)) + 1 in dom F by A11, FINSEQ_1:def_3; percases ( F . (((i -' 1) div (len b)) + 1) <> {} or F . (((i -' 1) div (len b)) + 1) = {} ) ; suppose F . (((i -' 1) div (len b)) + 1) <> {} ; ::_thesis: 0. <= x1 . i then consider x9 being set such that A164: x9 in F . (((i -' 1) div (len b)) + 1) by XBOOLE_0:def_1; ( FG . i in rng FG & rng FG c= S ) by A129, A155, FINSEQ_1:def_4, FUNCT_1:3; then reconsider FGi = FG . i as Element of S ; reconsider EMPTY = {} as Element of S by MEASURE1:7; EMPTY c= FGi by XBOOLE_1:2; then A165: M . {} <= M . FGi by MEASURE1:31; A166: F . (((i -' 1) div (len b)) + 1) c= dom f by A51, A163, FUNCT_1:3, ZFMISC_1:74; f . x9 = a . (((i -' 1) div (len b)) + 1) by A10, A163, A164, MESFUNC3:def_1 .= a1 . i by A48, A52, A157 ; then A167: 0. <= a1 . i by A3, A164, A166; M . {} = 0. by VALUED_0:def_19; then 0. <= (M * FG) . i by A129, A155, A165, FUNCT_1:13; hence 0. <= x1 . i by A156, A167; ::_thesis: verum end; supposeA168: F . (((i -' 1) div (len b)) + 1) = {} ; ::_thesis: 0. <= x1 . i FG . i = (F . (((i -' 1) div (len b)) + 1)) /\ (G . (((i -' 1) mod (len b)) + 1)) by A13, A129, A155; then M . (FG . i) = 0. by A168, VALUED_0:def_19; then (M * FG) . i = 0. by A129, A155, FUNCT_1:13; hence 0. <= x1 . i by A156; ::_thesis: verum end; end; end; not -infty in rng x1 proof assume -infty in rng x1 ; ::_thesis: contradiction then ex i being set st ( i in dom x1 & x1 . i = -infty ) by FUNCT_1:def_3; hence contradiction by A154; ::_thesis: verum end; then (x1 " {-infty}) /\ (y1 " {+infty}) = {} /\ (y1 " {+infty}) by FUNCT_1:72 .= {} ; then A169: dom (x1 + y1) = ((dom x1) /\ (dom y1)) \ ({} \/ {}) by A153, MESFUNC1:def_3 .= dom z1 by A129, A126, A135 ; A170: for k being Nat st k in dom z1 holds z1 . k = (x1 + y1) . k proof reconsider la9 = len a, lb9 = len b as Nat ; let k be Nat; ::_thesis: ( k in dom z1 implies z1 . k = (x1 + y1) . k ) set p = ((k -' 1) div (len b)) + 1; set q = ((k -' 1) mod (len b)) + 1; assume A171: k in dom z1 ; ::_thesis: z1 . k = (x1 + y1) . k then A172: k in Seg (len FG) by A135, FINSEQ_1:def_3; then A173: k <= (len a) * (len b) by A12, FINSEQ_1:1; then A174: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42; 1 <= k by A172, FINSEQ_1:1; then A175: ( lb9 divides la9 * lb9 & 1 <= (len a) * (len b) ) by A173, NAT_D:def_3, XXREAL_0:2; A176: len b <> 0 by A12, A172; then len b >= 0 + 1 by NAT_1:13; then ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A175, NAT_2:15; then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A174, NAT_2:24; then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19; then ( ((k -' 1) div (len b)) + 1 >= 0 + 1 & ((k -' 1) div (len b)) + 1 <= len a ) by A176, NAT_D:18, XREAL_1:6; then ((k -' 1) div (len b)) + 1 in Seg (len a) by FINSEQ_1:1; then A177: ((k -' 1) div (len b)) + 1 in dom F by A11, FINSEQ_1:def_3; (k -' 1) mod (len b) < len b by A176, NAT_D:1; then ( ((k -' 1) mod (len b)) + 1 >= 0 + 1 & ((k -' 1) mod (len b)) + 1 <= len b ) by NAT_1:13; then ((k -' 1) mod (len b)) + 1 in Seg (len b) by FINSEQ_1:1; then A178: ((k -' 1) mod (len b)) + 1 in dom G by A15, FINSEQ_1:def_3; A179: ((a1 . k) + (b1 . k)) * ((M * FG) . k) = ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) proof percases ( FG . k <> {} or FG . k = {} ) ; suppose FG . k <> {} ; ::_thesis: ((a1 . k) + (b1 . k)) * ((M * FG) . k) = ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) then (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) <> {} by A13, A135, A171; then consider v being set such that A180: v in (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by XBOOLE_0:def_1; A181: v in G . (((k -' 1) mod (len b)) + 1) by A180, XBOOLE_0:def_4; G . (((k -' 1) mod (len b)) + 1) in rng G by A178, FUNCT_1:3; then A182: v in dom g by A70, A181, TARSKI:def_4; b . (((k -' 1) mod (len b)) + 1) = g . v by A9, A178, A181, MESFUNC3:def_1; then 0. <= b . (((k -' 1) mod (len b)) + 1) by A6, A182; then A183: ( 0. = b1 . k or 0. < b1 . k ) by A50, A64, A172; A184: v in F . (((k -' 1) div (len b)) + 1) by A180, XBOOLE_0:def_4; F . (((k -' 1) div (len b)) + 1) in rng F by A177, FUNCT_1:3; then A185: v in dom f by A51, A184, TARSKI:def_4; a . (((k -' 1) div (len b)) + 1) = f . v by A10, A177, A184, MESFUNC3:def_1; then 0. <= a . (((k -' 1) div (len b)) + 1) by A3, A185; then ( 0. = a1 . k or 0. < a1 . k ) by A48, A52, A172; hence ((a1 . k) + (b1 . k)) * ((M * FG) . k) = ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A183, XXREAL_3:96; ::_thesis: verum end; suppose FG . k = {} ; ::_thesis: ((a1 . k) + (b1 . k)) * ((M * FG) . k) = ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) then M . (FG . k) = 0. by VALUED_0:def_19; then A186: (M * FG) . k = 0. by A135, A171, FUNCT_1:13; hence ((a1 . k) + (b1 . k)) * ((M * FG) . k) = 0 .= ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A186 ; ::_thesis: verum end; end; end; thus z1 . k = (c1 . k) * ((M * FG) . k) by A136, A171 .= ((a1 . k) * ((M * FG) . k)) + ((b1 . k) * ((M * FG) . k)) by A133, A137, A172, A179 .= (x1 . k) + ((b1 . k) * ((M * FG) . k)) by A129, A130, A135, A171 .= (x1 . k) + (y1 . k) by A126, A127, A135, A171 .= (x1 + y1) . k by A169, A171, MESFUNC1:def_3 ; ::_thesis: verum end; A187: dom (f + g) = (dom g) /\ (dom g) by A5, A7, MESFUNC2:2 .= dom g ; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(f_+_g)_holds_ |.((f_+_g)_._x).|_<_+infty let x be Element of X; ::_thesis: ( x in dom (f + g) implies |.((f + g) . x).| < +infty ) assume A188: x in dom (f + g) ; ::_thesis: |.((f + g) . x).| < +infty then |.((f + g) . x).| = |.((f . x) + (g . x)).| by MESFUNC1:def_3; then A189: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by EXTREAL2:13; g is V63() by A4, MESFUNC2:def_4; then A190: |.(g . x).| < +infty by A187, A188, MESFUNC2:def_1; f is V63() by A1, MESFUNC2:def_4; then |.(f . x).| < +infty by A8, A188, MESFUNC2:def_1; then |.(f . x).| + |.(g . x).| <> +infty by A190, XXREAL_3:16; hence |.((f + g) . x).| < +infty by A189, XXREAL_0:2, XXREAL_0:4; ::_thesis: verum end; then f + g is V63() by MESFUNC2:def_1; hence A191: f + g is_simple_func_in S by A71, A8, A107, MESFUNC2:def_4; ::_thesis: ( dom (f + g) <> {} & ( for x being set st x in dom (f + g) holds 0. <= (f + g) . x ) & integral (X,S,M,(f + g)) = (integral (X,S,M,f)) + (integral (X,S,M,g)) ) thus dom (f + g) <> {} by A2, A8; ::_thesis: ( ( for x being set st x in dom (f + g) holds 0. <= (f + g) . x ) & integral (X,S,M,(f + g)) = (integral (X,S,M,f)) + (integral (X,S,M,g)) ) thus A192: for x being set st x in dom (f + g) holds 0. <= (f + g) . x ::_thesis: integral (X,S,M,(f + g)) = (integral (X,S,M,f)) + (integral (X,S,M,g)) proof let x be set ; ::_thesis: ( x in dom (f + g) implies 0. <= (f + g) . x ) A193: dom f c= X by RELAT_1:def_18; assume A194: x in dom (f + g) ; ::_thesis: 0. <= (f + g) . x then ( 0. <= f . x & 0. <= g . x ) by A3, A6, A8, A187; then 0. <= (f . x) + (g . x) ; hence 0. <= (f + g) . x by A8, A194, A193, MESFUNC1:def_3; ::_thesis: verum end; dom FG = dom c1 by A132, FINSEQ_3:29; then FG,c1 are_Re-presentation_of f + g by A71, A8, A138, MESFUNC3:def_1; then A195: integral (X,S,M,(f + g)) = Sum z1 by A2, A135, A136, A8, A191, A192, Th3; dom (x1 + y1) = Seg (len z1) by A169, FINSEQ_1:def_3; then x1 + y1 is FinSequence by FINSEQ_1:def_2; then A196: z1 = x1 + y1 by A169, A170, FINSEQ_1:13; dom FG = Seg (len b1) by A49, FINSEQ_1:def_3 .= dom b1 by FINSEQ_1:def_3 ; then FG,b1 are_Re-presentation_of g by A5, A71, A65, MESFUNC3:def_1; then integral (X,S,M,g) = Sum y1 by A2, A4, A5, A6, A126, A127, Th3; hence integral (X,S,M,(f + g)) = (integral (X,S,M,f)) + (integral (X,S,M,g)) by A129, A126, A131, A195, A154, A143, A196, Th1; ::_thesis: verum end; theorem :: MESFUNC4:6 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL for c being R_eal st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & 0. <= c & c < +infty & dom g = dom f & ( for x being set st x in dom g holds g . x = c * (f . x) ) holds integral (X,S,M,g) = c * (integral (X,S,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, g being PartFunc of X,ExtREAL for c being R_eal st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & 0. <= c & c < +infty & dom g = dom f & ( for x being set st x in dom g holds g . x = c * (f . x) ) holds integral (X,S,M,g) = c * (integral (X,S,M,f)) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL for c being R_eal st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & 0. <= c & c < +infty & dom g = dom f & ( for x being set st x in dom g holds g . x = c * (f . x) ) holds integral (X,S,M,g) = c * (integral (X,S,M,f)) let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,ExtREAL for c being R_eal st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & 0. <= c & c < +infty & dom g = dom f & ( for x being set st x in dom g holds g . x = c * (f . x) ) holds integral (X,S,M,g) = c * (integral (X,S,M,f)) let f, g be PartFunc of X,ExtREAL; ::_thesis: for c being R_eal st f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & 0. <= c & c < +infty & dom g = dom f & ( for x being set st x in dom g holds g . x = c * (f . x) ) holds integral (X,S,M,g) = c * (integral (X,S,M,f)) let c be R_eal; ::_thesis: ( f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds 0. <= f . x ) & 0. <= c & c < +infty & dom g = dom f & ( for x being set st x in dom g holds g . x = c * (f . x) ) implies integral (X,S,M,g) = c * (integral (X,S,M,f)) ) assume that A1: f is_simple_func_in S and A2: dom f <> {} and A3: for x being set st x in dom f holds 0. <= f . x and A4: 0. <= c and A5: c < +infty and A6: dom g = dom f and A7: for x being set st x in dom g holds g . x = c * (f . x) ; ::_thesis: integral (X,S,M,g) = c * (integral (X,S,M,f)) A8: for x being set st x in dom g holds 0. <= g . x proof let x be set ; ::_thesis: ( x in dom g implies 0. <= g . x ) assume A9: x in dom g ; ::_thesis: 0. <= g . x then 0. <= f . x by A3, A6; then 0. <= c * (f . x) by A4; hence 0. <= g . x by A7, A9; ::_thesis: verum end; A10: ex G being Finite_Sep_Sequence of S st ( dom g = union (rng G) & ( for n being Nat for x, y being Element of X st n in dom G & x in G . n & y in G . n holds g . x = g . y ) ) proof consider G being Finite_Sep_Sequence of S such that A11: dom f = union (rng G) and A12: for n being Nat for x, y being Element of X st n in dom G & x in G . n & y in G . n holds f . x = f . y by A1, MESFUNC2:def_4; take G ; ::_thesis: ( dom g = union (rng G) & ( for n being Nat for x, y being Element of X st n in dom G & x in G . n & y in G . n holds g . x = g . y ) ) for n being Nat for x, y being Element of X st n in dom G & x in G . n & y in G . n holds g . x = g . y proof let n be Nat; ::_thesis: for x, y being Element of X st n in dom G & x in G . n & y in G . n holds g . x = g . y let x, y be Element of X; ::_thesis: ( n in dom G & x in G . n & y in G . n implies g . x = g . y ) assume that A13: n in dom G and A14: x in G . n and A15: y in G . n ; ::_thesis: g . x = g . y A16: G . n in rng G by A13, FUNCT_1:3; then y in dom g by A6, A11, A15, TARSKI:def_4; then A17: g . y = c * (f . y) by A7; x in dom g by A6, A11, A14, A16, TARSKI:def_4; then g . x = c * (f . x) by A7; hence g . x = g . y by A12, A13, A14, A15, A17; ::_thesis: verum end; hence ( dom g = union (rng G) & ( for n being Nat for x, y being Element of X st n in dom G & x in G . n & y in G . n holds g . x = g . y ) ) by A6, A11; ::_thesis: verum end; consider F being Finite_Sep_Sequence of S, a, x being FinSequence of ExtREAL such that A18: F,a are_Re-presentation_of f and A19: dom x = dom F and A20: for n being Nat st n in dom x holds x . n = (a . n) * ((M * F) . n) and A21: integral (X,S,M,f) = Sum x by A1, A2, A3, Th4; ex b being FinSequence of ExtREAL st ( dom b = dom a & ( for n being Nat st n in dom b holds b . n = c * (a . n) ) ) proof deffunc H1( Nat) -> Element of ExtREAL = c * (a . $1); consider b being FinSequence such that A22: ( len b = len a & ( for n being Nat st n in dom b holds b . n = H1(n) ) ) from FINSEQ_1:sch_2(); A23: rng b c= ExtREAL proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in rng b or v in ExtREAL ) assume v in rng b ; ::_thesis: v in ExtREAL then consider k being set such that A24: k in dom b and A25: v = b . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A24; v = c * (a . k) by A22, A24, A25; hence v in ExtREAL ; ::_thesis: verum end; A26: dom b = Seg (len b) by FINSEQ_1:def_3; reconsider b = b as FinSequence of ExtREAL by A23, FINSEQ_1:def_4; take b ; ::_thesis: ( dom b = dom a & ( for n being Nat st n in dom b holds b . n = c * (a . n) ) ) thus ( dom b = dom a & ( for n being Nat st n in dom b holds b . n = c * (a . n) ) ) by A22, A26, FINSEQ_1:def_3; ::_thesis: verum end; then consider b being FinSequence of ExtREAL such that A27: dom b = dom a and A28: for n being Nat st n in dom b holds b . n = c * (a . n) ; A29: c in REAL by A4, A5, XXREAL_0:14; ex z being FinSequence of ExtREAL st ( dom z = dom x & ( for n being Nat st n in dom z holds z . n = c * (x . n) ) ) proof deffunc H1( Nat) -> Element of ExtREAL = c * (x . $1); consider z being FinSequence such that A30: ( len z = len x & ( for n being Nat st n in dom z holds z . n = H1(n) ) ) from FINSEQ_1:sch_2(); A31: rng z c= ExtREAL proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in rng z or v in ExtREAL ) assume v in rng z ; ::_thesis: v in ExtREAL then consider k being set such that A32: k in dom z and A33: v = z . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A32; v = c * (x . k) by A30, A32, A33; hence v in ExtREAL ; ::_thesis: verum end; A34: dom z = Seg (len z) by FINSEQ_1:def_3; reconsider z = z as FinSequence of ExtREAL by A31, FINSEQ_1:def_4; take z ; ::_thesis: ( dom z = dom x & ( for n being Nat st n in dom z holds z . n = c * (x . n) ) ) thus ( dom z = dom x & ( for n being Nat st n in dom z holds z . n = c * (x . n) ) ) by A30, A34, FINSEQ_1:def_3; ::_thesis: verum end; then consider z being FinSequence of ExtREAL such that A35: dom z = dom x and A36: for n being Nat st n in dom z holds z . n = c * (x . n) ; A37: for n being Nat st n in dom z holds z . n = (b . n) * ((M * F) . n) proof let n be Nat; ::_thesis: ( n in dom z implies z . n = (b . n) * ((M * F) . n) ) A38: dom a = dom F by A18, MESFUNC3:def_1; assume A39: n in dom z ; ::_thesis: z . n = (b . n) * ((M * F) . n) hence z . n = c * (x . n) by A36 .= c * ((a . n) * ((M * F) . n)) by A20, A35, A39 .= (c * (a . n)) * ((M * F) . n) by XXREAL_3:66 .= (b . n) * ((M * F) . n) by A19, A27, A28, A35, A39, A38 ; ::_thesis: verum end; A40: dom g = union (rng F) by A6, A18, MESFUNC3:def_1; A41: now__::_thesis:_for_n_being_Nat_st_n_in_dom_F_holds_ for_x_being_set_st_x_in_F_._n_holds_ g_._x_=_b_._n let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds g . x = b . n ) assume A42: n in dom F ; ::_thesis: for x being set st x in F . n holds g . x = b . n then A43: n in dom b by A18, A27, MESFUNC3:def_1; let x be set ; ::_thesis: ( x in F . n implies g . x = b . n ) assume A44: x in F . n ; ::_thesis: g . x = b . n F . n in rng F by A42, FUNCT_1:3; then x in dom g by A40, A44, TARSKI:def_4; hence g . x = c * (f . x) by A7 .= c * (a . n) by A18, A42, A44, MESFUNC3:def_1 .= b . n by A28, A43 ; ::_thesis: verum end; dom F = dom b by A18, A27, MESFUNC3:def_1; then A45: F,b are_Re-presentation_of g by A40, A41, MESFUNC3:def_1; A46: f is V63() by A1, MESFUNC2:def_4; for x being Element of X st x in dom g holds |.(g . x).| < +infty proof let x be Element of X; ::_thesis: ( x in dom g implies |.(g . x).| < +infty ) assume A47: x in dom g ; ::_thesis: |.(g . x).| < +infty c * (f . x) <> -infty by A29, A46; then g . x <> -infty by A7, A47; then -infty < g . x by XXREAL_0:6; then A48: - +infty < g . x by XXREAL_3:def_3; c * (f . x) <> +infty by A29, A46; then g . x <> +infty by A7, A47; then g . x < +infty by XXREAL_0:4; hence |.(g . x).| < +infty by A48, EXTREAL2:11; ::_thesis: verum end; then g is V63() by MESFUNC2:def_1; then g is_simple_func_in S by A10, MESFUNC2:def_4; hence integral (X,S,M,g) = Sum z by A2, A6, A19, A8, A35, A45, A37, Th3 .= c * (integral (X,S,M,f)) by A29, A21, A35, A36, MESFUNC3:10 ; ::_thesis: verum end;