:: 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;