let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
defpred S₁[ 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 <> {} & f is nonnegative & 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 (M,f) = Sum x;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A2: S₁[n] ; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let F be Finite_Sep_Sequence of S; :: thesis:
let a, x be FinSequence of ExtREAL ; :: thesis:
assume that
A3: f is_simple_func_in S and
A4: dom f <> {} and
A5: f is nonnegative 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:
A10: f is V70() by A3, MESFUNC2:def 4;
a5: for x being object st x in dom f holds
0. <= f . x by A5, SUPINF_2:51;
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 ;
for x being object st x in dom (f | (union (rng (F | (Seg n))))) holds
0. <= (f | (union (rng (F | (Seg n))))) . x

end;

then a12: f | (union (rng (F | (Seg n)))) is nonnegative by SUPINF_2:52;
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:
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:
let x, y be Element of X; :: thesis:
assume that
A17: n in dom F1 and
A18: x in F1 . n and
A19: y in F1 . n ; :: thesis:
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:

end;

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 object st x in F1 . n holds
(f | (union (rng (F | (Seg n))))) . x = a1 . n

proof

let n be Nat; :: thesis:
assume A25: n in dom F1 ; :: thesis:
then A26: ( F1 . n = F . n & a1 . n = a . n ) by A24, FUNCT_1:47;
let x be object ; :: thesis:
assume A27: x in F1 . n ; :: thesis:
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:

end;

then A28: F1,a1 are_Re-presentation_of f | (union (rng (F | (Seg n)))) by A16, A24, MESFUNC3:def 1;

now :: thesis:

per cases ;

suppose A29: dom (f | (union (rng (F | (Seg n))))) = {} ; :: thesis:

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:

proof

let v be object ; :: according to TARSKI:def 3 :: thesis:
assume v in union (rng F) ; :: thesis:
then consider A being set such that
A32: v in A and
A33: A in rng F by TARSKI:def 4;
consider i being object 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;

per cases ;

suppose i = n + 1 ; :: thesis:

hence v in (union (rng F1)) \/ (F . (n + 1)) by A32, A35, XBOOLE_0:def 3; :: thesis:

end;

suppose i <> n + 1 ; :: thesis:

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:

end;

let v be object ; :: according to TARSKI:def 3 :: thesis:
assume A39: v in (union (rng F1)) \/ (F . (n + 1)) ; :: thesis:

per cases by A39, XBOOLE_0:def 3;

suppose v in union (rng F1) ; :: thesis:

then consider A being set such that
A40: v in A and
A41: A in rng F1 by TARSKI:def 4;
consider i being object 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:

end;

suppose A45: v in F . (n + 1) ; :: thesis:

F . (n + 1) in rng F by A30, FUNCT_1:3;
hence v in union (rng F) by A45, TARSKI:def 4; :: thesis:

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 sequence of ExtREAL such that
A49: Sum x = sumx . (len x) and
A50: sumx . 0 = 0. and
A51: for m being Nat st m < len x holds
sumx . (m + 1) = (sumx . m) + (x . (m + 1)) by EXTREAL1:def 2;
defpred S₂[ 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:
assume m in dom F1 ; :: thesis:
then F1 . m in rng F1 by FUNCT_1:3;
hence F1 . m = {} by A16, A29, XBOOLE_1:3, ZFMISC_1:74; :: thesis:

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:
assume A54: m in dom F1 ; :: thesis:
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:

end;

A58: for m being Nat st S₂[m] holds
S₂[m + 1]

proof

let m be Nat; :: thesis:
assume A59: S₂[m] ; :: thesis:
A60: 1 <= m + 1 by NAT_1:11;
assume A61: m + 1 < len x ; :: thesis:
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;
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
.= x . (m + 1) by XXREAL_3:4 ;
hence sumx . (m + 1) = 0. by A53, A63; :: thesis:

end;

A64: S₂[ 0 ] by A50;
A65: for m being Nat holds S₂[m] from NAT_1:sch 2(A64, A58);
A66: Sum x = sumx . (n + 1) by A49, A46, FINSEQ_1:6
.= (sumx . n) + (x . (n + 1)) by A51, A48
.= 0. + (x . (n + 1)) by A65, A48
.= x . (n + 1) by XXREAL_3:4 ;

now :: thesis:

per cases ;

case A67: a . (n + 1) <> 0. ; :: thesis:

defpred S₃[ Nat, set ] means ( ( $1 = 1 implies $2 = 0. ) & ( $1 = 2 implies $2 = a . (n + 1) ) );
defpred S₄[ Nat, set ] means ( ( $1 = 1 implies $2 = union (rng F1) ) & ( $1 = 2 implies $2 = F . (n + 1) ) );
A68: for k being Nat st k in Seg 2 holds
ex x being Element of ExtREAL st S₃[k,x]

proof

let k be Nat; :: thesis:
assume A69: k in Seg 2 ; :: thesis:

per cases by A69, FINSEQ_1:2, TARSKI:def 2;

suppose A70: k = 1 ; :: thesis:

set x = 0. ;
reconsider x = 0. as Element of ExtREAL ;
take x ; :: thesis:
thus S₃[k,x] by A70; :: thesis:

end;

suppose A71: k = 2 ; :: thesis:

set x = a . (n + 1);
reconsider x = a . (n + 1) as Element of ExtREAL ;
take x ; :: thesis:
thus S₃[k,x] by A71; :: thesis:

end;

consider b being FinSequence of ExtREAL such that
A72: ( dom b = Seg 2 & ( for k being Nat st k in Seg 2 holds
S₃[k,b . k] ) ) from FINSEQ_1:sch 5(A68);
A73: for k being Nat st k in Seg 2 holds
ex x being Element of S st S₄[k,x]

proof

let k be Nat; :: thesis:
assume A74: k in Seg 2 ; :: thesis:

per cases by A74, FINSEQ_1:2, TARSKI:def 2;

suppose A75: k = 1 ; :: thesis:

set x = union (rng F1);
reconsider x = union (rng F1) as Element of S by MESFUNC2:31;
take x ; :: thesis:
thus S₄[k,x] by A75; :: thesis:

end;

suppose A76: k = 2 ; :: thesis:

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:
thus S₄[k,x] by A76; :: thesis:

end;

consider G being FinSequence of S such that
A77: ( dom G = Seg 2 & ( for k being Nat st k in Seg 2 holds
S₄[k,G . k] ) ) from FINSEQ_1:sch 5(A73);
A78: 1 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then A79: b . 1 = 0. by A72;
A80: b . 1 = 0. by A72, A78;
2 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then A81: b . 2 = a . (n + 1) by A72;
A82: 2 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then A83: G . 2 = F . (n + 1) by A77;
A84: 1 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then A85: G . 1 = union (rng F1) by A77;
A86: for u, v being object st u <> v holds
G . u misses G . v

proof

let u, v be object ; :: thesis:
assume A87: u <> v ; :: thesis:

per cases ;

suppose A88: ( u in dom G & v in dom G ) ; :: thesis:

then A89: ( u = 1 or u = 2 ) by A77, FINSEQ_1:2, TARSKI:def 2;

per cases by A77, A87, A88, A89, FINSEQ_1:2, TARSKI:def 2;

suppose A90: ( u = 1 & v = 2 ) ; :: thesis:

assume G . u meets G . v ; :: thesis:
then consider z being object such that
A91: z in G . u and
A92: z in G . v by XBOOLE_0:3;
consider A being set such that
A93: z in A and
A94: A in rng F1 by A85, A90, A91, TARSKI:def 4;
consider k9 being object such that
A95: k9 in dom F1 and
A96: A = F1 . k9 by A94, FUNCT_1:def 3;
reconsider k9 = k9 as Element of NAT by A95;
A97: z in F . k9 by A93, A95, A96, FUNCT_1:47;
k9 in (dom F) /\ (Seg n) by A95, 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 A98: F . k9 misses F . (n + 1) by PROB_2:def 2;
z in F . (n + 1) by A77, A82, A90, A92;
hence contradiction by A98, A97, XBOOLE_0:3; :: thesis:

end;

suppose A99: ( u = 2 & v = 1 ) ; :: thesis:

assume G . u meets G . v ; :: thesis:
then consider z being object such that
A100: z in G . u and
A101: z in G . v by XBOOLE_0:3;
consider A being set such that
A102: z in A and
A103: A in rng F1 by A85, A99, A101, TARSKI:def 4;
consider k9 being object such that
A104: k9 in dom F1 and
A105: A = F1 . k9 by A103, FUNCT_1:def 3;
reconsider k9 = k9 as Element of NAT by A104;
A106: z in F . k9 by A102, A104, A105, FUNCT_1:47;
k9 in (dom F) /\ (Seg n) by A104, 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 A107: F . k9 misses F . (n + 1) by PROB_2:def 2;
z in F . (n + 1) by A77, A82, A99, A100;
hence contradiction by A107, A106, XBOOLE_0:3; :: thesis:

end;

suppose ( not u in dom G or not v in dom G ) ; :: thesis:

then ( G . u = {} or G . v = {} ) by FUNCT_1:def 2;
hence G . u misses G . v ; :: thesis:

end;

len G = 2 by A77, FINSEQ_1:def 3;
then A108: G = <*(union (rng F1)),(F . (n + 1))*> by A85, A83, FINSEQ_1:44;
deffunc H₁( Nat) -> Element of ExtREAL = (b . $1) * ((M * G) . $1);
consider y being FinSequence of ExtREAL such that
A109: ( len y = 2 & ( for m being Nat st m in dom y holds
y . m = H₁(m) ) ) from FINSEQ_2:sch 1();
A110: dom y = Seg 2 by A109, FINSEQ_1:def 3;
1 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then A111: y . 1 = (b . 1) * ((M * G) . 1) by A109, A110;
consider sumy being sequence of ExtREAL such that
A112: Sum y = sumy . (len y) and
A113: sumy . 0 = 0. and
A114: for k being Nat st k < len y holds
sumy . (k + 1) = (sumy . k) + (y . (k + 1)) by EXTREAL1:def 2;
A115: sumy . 1 = (sumy . 0) + (y . (0 + 1)) by A109, A114
.= 0. by A79, A111, A113 ;
A116: 2 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then (M * G) . 2 = M . (F . (n + 1)) by A77, A83, FUNCT_1:13
.= (M * F) . (n + 1) by A30, FUNCT_1:13 ;
then y . 2 = (a . (n + 1)) * ((M * F) . (n + 1)) by A81, A109, A110, A116;
then A117: y . 2 = x . (n + 1) by A7, A8, A30;
reconsider G = G as Finite_Sep_Sequence of S by A86, PROB_2:def 2;
A118: dom y = dom G by A77, A109, FINSEQ_1:def 3;
A119: for k being Nat st k in dom G holds
for v being object st v in G . k holds
f . v = b . k

proof

let k be Nat; :: thesis:
assume A120: k in dom G ; :: thesis:
let v be object ; :: thesis:
assume A121: v in G . k ; :: thesis:

per cases by A77, A120, FINSEQ_1:2, TARSKI:def 2;

suppose k = 1 ; :: thesis:

hence f . v = b . k by A16, A29, A77, A84, A121; :: thesis:

end;

suppose k = 2 ; :: thesis:

hence f . v = b . k by A6, A30, A83, A81, A121, MESFUNC3:def 1; :: thesis:

end;

A122: for k being Nat st 2 <= k & k in dom b holds
( 0. < b . k & b . k < +infty )

proof

let k be Nat; :: thesis:
assume that
A123: 2 <= k and
A124: k in dom b ; :: thesis:
A125: ( k = 1 or k = 2 ) by A72, A124, FINSEQ_1:2, TARSKI:def 2;
then G . k <> {} by A4, A6, A11, A29, A31, A83, A123, MESFUNC3:def 1;
then consider v being object such that
A126: v in G . k by XBOOLE_0:def 1;
A127: v in dom f by A6, A16, A29, A31, A83, A123, A125, A126, MESFUNC3:def 1;
A128: f . v = b . k by A77, A72, A119, A124, A126;
hence 0. < b . k by A67, A81, A123, A125, A127, a5; :: thesis:
dom f c= X by RELAT_1:def 18;
then reconsider v = v as Element of X by A127;
|.(f . v).| < +infty by A10, A127, MESFUNC2:def 1;
hence b . k < +infty by A128, EXTREAL1:21; :: thesis:

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 A108, FINSEQ_2:127 ;
then A129: G,b are_Re-presentation_of f by A77, A72, A119, MESFUNC3:def 1;
Sum y = sumy . (1 + 1) by A109, A112
.= 0. + (x . (n + 1)) by A109, A117, A114, A115
.= x . (n + 1) by XXREAL_3:4 ;
hence integral (M,f) = Sum x by A3, A5, A66, A109, A122, A129, A80, A118, MESFUNC3:def 2; :: thesis:

end;

case A130: a . (n + 1) = 0. ; :: thesis:

defpred S₃[ Nat, set ] means ( ( $1 = 1 implies $2 = 0. ) & ( $1 = 2 implies $2 = 1. ) );
defpred S₄[ Nat, set ] means ( ( $1 = 1 implies $2 = union (rng F) ) & ( $1 = 2 implies $2 = {} ) );
A131: for k being Nat st k in Seg 2 holds
ex v being Element of S st S₄[k,v]

proof

let k be Nat; :: thesis:
assume A132: k in Seg 2 ; :: thesis:

per cases by A132, FINSEQ_1:2, TARSKI:def 2;

suppose A133: k = 1 ; :: thesis:

set v = union (rng F);
reconsider v = union (rng F) as Element of S by MESFUNC2:31;
take v ; :: thesis:
thus S₄[k,v] by A133; :: thesis:

end;

suppose A134: k = 2 ; :: thesis:

reconsider v = {} as Element of S by PROB_1:4;
take v ; :: thesis:
thus S₄[k,v] by A134; :: thesis:

end;

consider G being FinSequence of S such that
A135: ( dom G = Seg 2 & ( for k being Nat st k in Seg 2 holds
S₄[k,G . k] ) ) from FINSEQ_1:sch 5(A131);
A136: for u, v being object st u <> v holds
G . u misses G . v

proof

let u, v be object ; :: thesis:
assume A137: u <> v ; :: thesis:

per cases ;

suppose A138: ( u in dom G & v in dom G ) ; :: thesis:

then A139: ( u = 1 or u = 2 ) by A135, FINSEQ_1:2, TARSKI:def 2;

per cases by A135, A137, A138, A139, FINSEQ_1:2, TARSKI:def 2;

suppose ( u = 1 & v = 2 ) ; :: thesis:

then G . v = {} by A135, A138;
hence G . u misses G . v ; :: thesis:

end;

suppose ( u = 2 & v = 1 ) ; :: thesis:

then G . u = {} by A135, A138;
hence G . u misses G . v ; :: thesis:

end;

suppose ( not u in dom G or not v in dom G ) ; :: thesis:

then ( G . u = {} or G . v = {} ) by FUNCT_1:def 2;
hence G . u misses G . v ; :: thesis:

end;

A140: for k being Nat st k in Seg 2 holds
ex v being Element of ExtREAL st S₃[k,v]

proof

let k be Nat; :: thesis:
assume A141: k in Seg 2 ; :: thesis:

per cases by A141, FINSEQ_1:2, TARSKI:def 2;

suppose A142: k = 1 ; :: thesis:

set v = 0. ;
reconsider v = 0. as Element of ExtREAL ;
take v ; :: thesis:
thus S₃[k,v] by A142; :: thesis:

end;

suppose A143: k = 2 ; :: thesis:

set v = 1. ;
reconsider v = 1. as Element of ExtREAL ;
take v ; :: thesis:
thus S₃[k,v] by A143; :: thesis:

end;

consider b being FinSequence of ExtREAL such that
A144: ( dom b = Seg 2 & ( for k being Nat st k in Seg 2 holds
S₃[k,b . k] ) ) from FINSEQ_1:sch 5(A140);
A145: 2 in dom G by A135, FINSEQ_1:2, TARSKI:def 2;
then A146: G . 2 = {} by A135;
M . (G . 2) = (M * G) . 2 by A145, FUNCT_1:13;
then A147: (M * G) . 2 = 0. by A146, VALUED_0:def 19;
1 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then A148: G . 1 = union (rng F) by A135;
A149: 1 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then A150: b . 1 = 0. by A144;
deffunc H₁( Nat) -> Element of ExtREAL = (b . $1) * ((M * G) . $1);
consider y being FinSequence of ExtREAL such that
A151: ( len y = 2 & ( for k being Nat st k in dom y holds
y . k = H₁(k) ) ) from FINSEQ_2:sch 1();
A152: dom y = Seg 2 by A151, FINSEQ_1:def 3;
2 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then A153: y . 2 = (b . 2) * ((M * G) . 2) by A151, A152;
1 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then A154: y . 1 = (b . 1) * ((M * G) . 1) by A151, A152;
reconsider G = G as Finite_Sep_Sequence of S by A136, PROB_2:def 2;
A155: dom y = dom G by A135, A151, FINSEQ_1:def 3;
A156: for k being Nat st k in dom G holds
for v being object st v in G . k holds
f . v = b . k

proof

let k be Nat; :: thesis:
assume A157: k in dom G ; :: thesis:
let v be object ; :: thesis:
assume A158: v in G . k ; :: thesis:

per cases by A135, A157, FINSEQ_1:2, TARSKI:def 2;

suppose A159: k = 1 ; :: thesis:

then f . v = 0. by A6, A16, A29, A30, A31, A130, A148, A158, MESFUNC3:def 1;
hence f . v = b . k by A144, A149, A159; :: thesis:

end;

suppose k = 2 ; :: thesis:

hence f . v = b . k by A135, A145, A158; :: thesis:

end;

len G = 2 by A135, FINSEQ_1:def 3;
then G = <*(union (rng F)),{}*> by A148, A146, 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 A160: G,b are_Re-presentation_of f by A135, A144, A156, MESFUNC3:def 1;
consider sumy being sequence of ExtREAL such that
A161: Sum y = sumy . (len y) and
A162: sumy . 0 = 0. and
A163: for k being Nat st k < len y holds
sumy . (k + 1) = (sumy . k) + (y . (k + 1)) by EXTREAL1:def 2;
A164: sumy . 1 = (sumy . 0) + (y . (0 + 1)) by A151, A163
.= 0. by A150, A154, A162 ;
A165: 2 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
A166: for k being Nat st 2 <= k & k in dom b holds
( 0. < b . k & b . k < +infty )

proof

let k be Nat; :: thesis:
assume that
A167: 2 <= k and
A168: k in dom b ; :: thesis:
( k = 1 or k = 2 ) by A144, A168, FINSEQ_1:2, TARSKI:def 2;
hence 0. < b . k by A144, A165, A167; :: thesis:
A169: 1 in REAL by NUMBERS:19;
S₃[k,b . k] by A144, A149, A165;
then ( b . k = 1 or b . k = 0. ) by A144, A168, FINSEQ_1:2, TARSKI:def 2;
hence b . k < +infty by XXREAL_0:9, A169; :: thesis:

end;

A170: b . 1 = 0. by A144, A149;
( 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 A130 ;
Sum y = (sumy . 1) + (y . (1 + 1)) by A151, A161, A163
.= 0. by A147, A153, A164 ;
hence integral (M,f) = Sum x by A3, A5, A66, A171, A151, A166, A160, A170, A155, MESFUNC3:def 2; :: thesis:

end;

hence integral (M,f) = Sum x ; :: thesis:

end;

suppose A172: dom (f | (union (rng (F | (Seg n))))) <> {} ; :: thesis:

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 (M,(f | (union (rng (F | (Seg n)))))) = Sum y by A23, MESFUNC3:def 2, a12;
A183: for i being Nat st i in dom x1 holds
x1 . i = (a1 . i) * ((M * F1) . i)

proof

let i be Nat; :: thesis:
assume A184: i in dom x1 ; :: thesis:
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:

end;

now :: thesis:

per cases ;

case A187: ( F . (n + 1) = {} or a . (n + 1) = 0. ) ; :: thesis:

defpred S₂[ 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 S₂[k,x]

proof

let k be Nat; :: thesis:
A189: rng G c= S by FINSEQ_1:def 4;
assume k in Seg (len G) ; :: thesis:
then k in dom G by FINSEQ_1:def 3;
then A190: G . k in rng G by FUNCT_1:3;

per cases ;

suppose A191: k = 1 ; :: thesis:

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;
S₂[k,x] by A191;
hence ex x being Element of S st S₂[k,x] ; :: thesis:

end;

suppose A193: k <> 1 ; :: thesis:

set x = G . k;
reconsider x = G . k as Element of S by A190, A189;
S₂[k,x] by A193;
hence ex x being Element of S st S₂[k,x] ; :: thesis:

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
S₂[k,H . k] ) ) from FINSEQ_1:sch 5(A188);
A195: for u, v being object st u <> v holds
H . u misses H . v

proof

let u, v be object ; :: thesis:
assume A196: u <> v ; :: thesis:

per cases ;

suppose A197: ( u in dom H & v in dom H ) ; :: thesis:

then reconsider u1 = u, v1 = v as Element of NAT ;

per cases ;

suppose A198: u = 1 ; :: thesis:

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

per cases by A187;

suppose F . (n + 1) = {} ; :: thesis:

hence F . (n + 1) misses G . v ; :: thesis:

end;

suppose A202: a . (n + 1) = 0. ; :: thesis:

assume F . (n + 1) meets G . v ; :: thesis:
then consider w being object 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:

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:

end;

suppose A208: u <> 1 ; :: thesis:

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;

per cases ;

suppose A211: v = 1 ; :: thesis:

A212: F . (n + 1) misses G . u

proof

per cases by A187;

suppose F . (n + 1) = {} ; :: thesis:

hence F . (n + 1) misses G . u ; :: thesis:

end;

suppose A213: a . (n + 1) = 0. ; :: thesis:

assume F . (n + 1) meets G . u ; :: thesis:
then consider w being object 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:

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:

end;

suppose A219: v <> 1 ; :: thesis:

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:

end;

suppose ( not u in dom H or not v in dom H ) ; :: thesis:

then ( H . u = {} or H . v = {} ) by FUNCT_1:def 2;
hence H . u misses H . v ; :: thesis:

end;

deffunc H₁( 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 = H₁(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:

proof

let v be object ; :: according to TARSKI:def 3 :: thesis:
assume v in dom f ; :: thesis:
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 object 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;

per cases ;

suppose u = n + 1 ; :: thesis:

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:

end;

suppose u <> n + 1 ; :: thesis:

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

per cases ;

suppose A236: w = 1 ; :: thesis:

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:

end;

suppose A238: w <> 1 ; :: thesis:

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:

end;

let v be object ; :: according to TARSKI:def 3 :: thesis:
assume v in union (rng H) ; :: thesis:
then consider A being set such that
A240: v in A and
A241: A in rng H by TARSKI:def 4;
consider k being object 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;

per cases ;

suppose k = 1 ; :: thesis:

then A244: H . k = (G . 1) \/ (F . (n + 1)) by A194, A242;

per cases by A240, A243, A244, XBOOLE_0:def 3;

suppose A245: v in G . 1 ; :: thesis:

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:

end;

suppose A246: v in F . (n + 1) ; :: thesis:

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:

end;

suppose A247: k <> 1 ; :: thesis:

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:

end;

A249: now :: thesis:

assume -infty in rng x1 ; :: thesis:
then consider l being object 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;

per cases ;

suppose A254: F . l <> {} ; :: thesis:

reconsider EMPTY = {} as Element of S by MEASURE1:7;
consider v being object 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 ;
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 A257, a5;
hence contradiction by A253, A258; :: thesis:

end;

suppose A259: F . l = {} ; :: thesis:

(M * F) . l = M . (F . l) by A7, A252, FUNCT_1:13
.= 0. by A259, VALUED_0:def 19 ;
hence contradiction by A253; :: thesis:

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

per cases by A187;

suppose A262: F . (n + 1) = {} ; :: thesis:

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

end;

suppose A264: a . (n + 1) = 0. ; :: thesis:

x . (n + 1) = (a . (n + 1)) * ((M * F) . (n + 1)) by A7, A8, A260;
hence x . (n + 1) = 0. by A264; :: thesis:

end;

A265: now :: thesis:

assume -infty in rng <*(x . (n + 1))*> ; :: thesis:
then -infty in {(x . (n + 1))} by FINSEQ_1:39;
hence contradiction by A261; :: thesis:

end;

A266: for m being Nat st m in dom H holds
for x being object st x in H . m holds
f . x = b . m

proof

let m be Nat; :: thesis:
assume A267: m in dom H ; :: thesis:
let x be object ; :: thesis:
assume A268: x in H . m ; :: thesis:

per cases ;

suppose A269: m = 1 ; :: thesis:

then A270: H . m = (G . 1) \/ (F . (n + 1)) by A194, A267;

per cases by A268, A270, XBOOLE_0:def 3;

suppose A271: x in G . 1 ; :: thesis:

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:

end;

suppose A274: x in F . (n + 1) ; :: thesis:

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:

end;

suppose A275: m <> 1 ; :: thesis:

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:

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:
assume A282: k in dom z ; :: thesis:
then A283: z . k = (b . k) * ((M * H) . k) by A220;
A284: y . k = (b . k) * ((M * G) . k) by A181, A279, A282;

per cases ;

suppose A285: k = 1 ; :: thesis:

then z . k = 0. by A178, A283;
hence z . k = y . k by A178, A284, A285; :: thesis:

end;

suppose A286: k <> 1 ; :: thesis:

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:

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 (M,f) = Sum z by A3, A5, A178, A179, A220, A280, MESFUNC3:def 2
.= integral (M,(f | (union (rng (F | (Seg n)))))) by A182, A279, A281, FINSEQ_1:13
.= Sum x1 by A2, A23, A28, A14, A172, A183, A176, a12
.= Sum x by A289, XXREAL_3:4 ;
hence integral (M,f) = Sum x ; :: thesis:

end;

case A290: ( F . (n + 1) <> {} & a . (n + 1) <> 0. ) ; :: thesis:

defpred S₂[ Nat, set ] means ( ( $1 <= len b implies $2 = b . $1 ) & ( $1 = (len b) + 1 implies $2 = a . (n + 1) ) );
A291: f is V70() by A3, MESFUNC2:def 4;
consider v being object 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 S₂[k,v]

proof

let k be Nat; :: thesis:
assume k in Seg ((len b) + 1) ; :: thesis:

per cases ;

suppose A294: k <> (len b) + 1 ; :: thesis:

reconsider v = b . k as Element of ExtREAL ;
take v ; :: thesis:
thus S₂[k,v] by A294; :: thesis:

end;

suppose A295: k = (len b) + 1 ; :: thesis:

reconsider v = a . (n + 1) as Element of ExtREAL ;
take v ; :: thesis:
thus S₂[k,v] by A295, NAT_1:13; :: thesis:

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
S₂[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 EXTREAL1:21;
A300: len c = (len b) + 1 by A296, FINSEQ_1:def 3;
A301: 0. <= f . v by A298, a5;
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:
assume that
A304: 2 <= m and
A305: m in dom c ; :: thesis:
A306: m <= len c by A305, FINSEQ_3:25;

per cases ;

suppose m = len c ; :: thesis:

hence ( 0. < c . m & c . m < +infty ) by A302, A299, A296, A300, A305; :: thesis:

end;

suppose m <> len c ; :: thesis:

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:

end;

A309: 0. <= a . (n + 1) by A6, A297, A292, A301, MESFUNC3:def 1;

A310: now :: thesis:

assume A311: ( -infty in rng y or -infty in rng <*((a . (n + 1)) * ((M * F) . (n + 1)))*> ) ; :: thesis:

per cases by A311;

suppose -infty in rng y ; :: thesis:

then consider k being object 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;

per cases ;

suppose k = 1 ; :: thesis:

hence contradiction by A178, A313, A314; :: thesis:

end;

suppose k <> 1 ; :: thesis:

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:

end;

suppose A319: -infty in rng <*((a . (n + 1)) * ((M * F) . (n + 1)))*> ; :: thesis:

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:

end;

A324: not -infty in rng x1

proof

reconsider EMPTY = {} as Element of S by PROB_1:4;
assume -infty in rng x1 ; :: thesis:
then consider k being object 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;

per cases ;

suppose F . k <> {} ; :: thesis:

then consider v being object 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 A331, a5;
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:

end;

suppose F . k = {} ; :: thesis:

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:

end;

defpred S₃[ 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 S₃[k,v]

proof

let k be Nat; :: thesis:
assume A338: k in Seg ((len G) + 1) ; :: thesis:

per cases ;

suppose A339: k <> (len G) + 1 ; :: thesis:

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:
thus S₃[k,v] by A339; :: thesis:

end;

suppose A342: k = (len G) + 1 ; :: thesis:

( 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:
thus S₃[k,v] by A342, NAT_1:13; :: thesis:

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
S₃[k,H . k] ) ) from FINSEQ_1:sch 5(A337);
A344: for i, j being object st i <> j holds
H . i misses H . j

proof

let i, j be object ; :: thesis:
assume A345: i <> j ; :: thesis:

per cases ;

suppose A346: ( i in dom H & j in dom H ) ; :: thesis:

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:
then consider v being object 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 object 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)) = {} ;
hence contradiction by A352, A353, XBOOLE_0:def 4; :: thesis:

end;

let k be Nat; :: thesis:
assume that
A358: 1 <= k and
A359: k <= len G ; :: thesis:
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:

end;

A361: 1 <= j by A343, A346, FINSEQ_1:1;
A362: i <= (len G) + 1 by A343, A346, FINSEQ_1:1;
A363: S₃[i,H . i] by A343, A346;
A364: S₃[j,H . j] by A343, A346;

per cases ;

suppose A365: i = (len G) + 1 ; :: thesis:

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:

end;

suppose i <> (len G) + 1 ; :: thesis:

then A366: i < (len G) + 1 by A362, XXREAL_0:1;
then A367: i <= len G by NAT_1:13;

per cases ;

suppose j = (len G) + 1 ; :: thesis:

hence H . i misses H . j by A347, A364, A349, A367; :: thesis:

end;

suppose j <> (len G) + 1 ; :: thesis:

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:

end;

suppose A368: ( not i in dom H or not j in dom H ) ; :: thesis:

per cases by A368;

suppose not i in dom H ; :: thesis:

then H . i = {} by FUNCT_1:def 2;
hence H . i misses H . j ; :: thesis:

end;

suppose not j in dom H ; :: thesis:

then H . j = {} by FUNCT_1:def 2;
hence H . i misses H . j ; :: thesis:

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 S₄[ 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 S₄[k,v]

proof

let k be Nat; :: thesis:
assume k in Seg ((len y) + 1) ; :: thesis:

per cases ;

suppose A372: k <> (len y) + 1 ; :: thesis:

reconsider v = (b . k) * ((M * H) . k) as Element of ExtREAL ;
take v ; :: thesis:
thus S₄[k,v] by A372; :: thesis:

end;

suppose A373: k = (len y) + 1 ; :: thesis:

reconsider v = (a . (n + 1)) * ((M * F) . (n + 1)) as Element of ExtREAL ;
take v ; :: thesis:
thus S₄[k,v] by A373, NAT_1:13; :: thesis:

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
S₄[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:
assume A381: m in dom z ; :: thesis:
then A382: S₂[m,c . m] by A296, A336, A374, A375;

per cases ;

suppose m = (len y) + 1 ; :: thesis:

hence z . m = (c . m) * ((M * H) . m) by A335, A374, A375, A376, A379, A381, A382, FINSEQ_1:6; :: thesis:

end;

suppose A383: m <> (len y) + 1 ; :: thesis:

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:

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:
assume that
A389: 1 <= k and
A390: k <= len z ; :: thesis:

per cases ;

suppose k = len z ; :: thesis:

hence z . k = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k by A386, A387, FINSEQ_1:42; :: thesis:

end;

suppose k <> len z ; :: thesis:

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:

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

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:
assume that
A400: 1 <= k and
A401: k <= len H ; :: thesis:
k in Seg ((len G) + 1) by A370, A400, A401, FINSEQ_1:1;
then A402: S₃[k,H . k] by A343;

per cases ;

suppose k = (len G) + 1 ; :: thesis:

hence H . k = (G ^ <*(F . (n + 1))*>) . k by A402, FINSEQ_1:42; :: thesis:

end;

suppose k <> (len G) + 1 ; :: thesis:

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:

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 object st v in H . m holds
f . v = c . m

proof

let m be Nat; :: thesis:
assume A406: m in dom H ; :: thesis:
then A407: S₃[m,H . m] by A343;
A408: m <= (len G) + 1 by A343, A406, FINSEQ_1:1;
let v be object ; :: thesis:
assume A409: v in H . m ; :: thesis:
A410: S₂[m,c . m] by A343, A296, A336, A406;
A411: 1 <= m by A343, A406, FINSEQ_1:1;

per cases ;

suppose A412: m = (len G) + 1 ; :: thesis:

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:

end;

suppose m <> (len G) + 1 ; :: thesis:

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:

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 (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 (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, A28, A14, A172, A183, A176, A379, a12
.= (Sum x1) + (Sum <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) by EXTREAL1:8
.= Sum x by A310, A324, A397, EXTREAL1:10 ;
hence integral (M,f) = Sum x ; :: thesis:

end;

hence integral (M,f) = Sum x ; :: thesis:

end;

hence integral (M,f) = Sum x ; :: thesis:

end;

A419: S₁[ 0 ]

proof

let f be PartFunc of X,ExtREAL; :: thesis:
let F be Finite_Sep_Sequence of S; :: thesis:
let a, x be FinSequence of ExtREAL ; :: thesis:
assume that
f is_simple_func_in S and
A420: dom f <> {} and
f is nonnegative 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:
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 (M,f) = Sum x by A420, A421, MESFUNC3:def 1; :: thesis:

end;

for n being Nat holds S₁[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 <> {} & f is nonnegative & 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 (M,f) = Sum x ; :: thesis: