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 <> {} & 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

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 <> {} & 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

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 <> {} & 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

defpred S_{1}[ 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_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[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: verum

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 <> {} & 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

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 <> {} & 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

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 <> {} & 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

defpred 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 <> {} & 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

S

proof

A419:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[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 <> {} & 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 + 1 holds

integral (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 <> {} & 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 + 1 holds

integral (M,f) = Sum x

let a, x be FinSequence of ExtREAL ; :: thesis: ( 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 + 1 implies integral (M,f) = Sum x )

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: integral (M,f) = Sum x

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

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

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

end;assume A2: S

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 <> {} & 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 + 1 holds

integral (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 <> {} & 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 + 1 holds

integral (M,f) = Sum x

let a, x be FinSequence of ExtREAL ; :: thesis: ( 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 + 1 implies integral (M,f) = Sum x )

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: integral (M,f) = Sum x

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

proof

then a12:
f | (union (rng (F | (Seg n)))) is nonnegative
by SUPINF_2:52;
let x be object ; :: thesis: ( x in dom (f | (union (rng (F | (Seg n))))) implies 0. <= (f | (union (rng (F | (Seg n))))) . x )

assume x in dom (f | (union (rng (F | (Seg n))))) ; :: thesis: 0. <= (f | (union (rng (F | (Seg n))))) . x

then X: ( 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;

0. <= f . x by A5, SUPINF_2:51;

hence 0. <= (f | (union (rng (F | (Seg n))))) . x by X; :: thesis: verum

end;assume x in dom (f | (union (rng (F | (Seg n))))) ; :: thesis: 0. <= (f | (union (rng (F | (Seg n))))) . x

then X: ( 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;

0. <= f . x by A5, SUPINF_2:51;

hence 0. <= (f | (union (rng (F | (Seg n))))) . x by X; :: thesis: verum

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

then A23:
f | (union (rng (F | (Seg n)))) is_simple_func_in S
by A10, MESFUNC2:def 4;
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

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

hence
( dom (f | (union (rng (F | (Seg n))))) = union (rng F1) & ( for n being Nat
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;(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

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

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

then A28:
F1,a1 are_Re-presentation_of f | (union (rng (F | (Seg n))))
by A16, A24, MESFUNC3:def 1;
let n be Nat; :: thesis: ( n in dom F1 implies for x being object 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 object 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 object ; :: 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;(f | (union (rng (F | (Seg n))))) . x = a1 . n )

assume A25: n in dom F1 ; :: thesis: for x being object 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 object ; :: 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

now :: thesis: integral (M,f) = Sum xend;

hence
integral (M,f) = Sum x
; :: thesis: verumper cases
( dom (f | (union (rng (F | (Seg n))))) = {} or dom (f | (union (rng (F | (Seg n))))) <> {} )
;

end;

suppose A29:
dom (f | (union (rng (F | (Seg n))))) = {}
; :: thesis: integral (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))

.= 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_{2}[ Nat] means ( $1 < len x implies sumx . $1 = 0. );

A52: for m being Nat st m in dom F1 holds

F1 . m = {}

x . m = 0._{2}[m] holds

S_{2}[m + 1]
_{2}[ 0 ]
by A50;

A65: for m being Nat holds S_{2}[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 ;

end;then A30: n + 1 in dom F by A9, FINSEQ_3:25;

A31: union (rng F) = (union (rng F1)) \/ (F . (n + 1))

proof

A46: Seg (len x) =
dom F
by A7, FINSEQ_1:def 3
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)

assume A39: v in (union (rng F1)) \/ (F . (n + 1)) ; :: thesis: v in union (rng F)

end;proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in (union (rng F1)) \/ (F . (n + 1)) or v in union (rng F) )
let v be object ; :: 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 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;

end;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 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
( i = n + 1 or i <> n + 1 )
;

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

assume A39: v in (union (rng F1)) \/ (F . (n + 1)) ; :: thesis: v in union (rng F)

per cases
( v in union (rng F1) or v in F . (n + 1) )
by A39, XBOOLE_0:def 3;

end;

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

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

.= 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

A52: for m being Nat st m in dom F1 holds

F1 . m = {}

proof

A53:
for m being Nat st m in dom F1 holds
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;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

x . m = 0.

proof

A58:
for m being Nat st S
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;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

S

proof

A64:
S
let m be Nat; :: thesis: ( S_{2}[m] implies S_{2}[m + 1] )

assume A59: S_{2}[m]
; :: thesis: S_{2}[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;

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

end;assume A59: S

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;

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

A65: for m being Nat holds S

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: ( ( a . (n + 1) <> 0. & integral (M,f) = Sum x ) or ( a . (n + 1) = 0. & integral (M,f) = Sum x ) )end;

hence
integral (M,f) = Sum x
; :: thesis: verumper cases
( a . (n + 1) <> 0. or a . (n + 1) = 0. )
;

end;

case A67:
a . (n + 1) <> 0.
; :: thesis: integral (M,f) = Sum x

defpred S_{3}[ Nat, set ] means ( ( $1 = 1 implies $2 = 0. ) & ( $1 = 2 implies $2 = a . (n + 1) ) );

defpred S_{4}[ 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_{3}[k,x]

A72: ( dom b = Seg 2 & ( for k being Nat st k in Seg 2 holds

S_{3}[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_{4}[k,x]

A77: ( dom G = Seg 2 & ( for k being Nat st k in Seg 2 holds

S_{4}[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

then A108: G = <*(union (rng F1)),(F . (n + 1))*> by A85, A83, FINSEQ_1:44;

deffunc H_{1}( 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_{1}(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

( 0. < b . k & b . k < +infty )

.= 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: verum

end;defpred S

A68: for k being Nat st k in Seg 2 holds

ex x being Element of ExtREAL st S

proof

consider b being FinSequence of ExtREAL such that
let k be Nat; :: thesis: ( k in Seg 2 implies ex x being Element of ExtREAL st S_{3}[k,x] )

assume A69: k in Seg 2 ; :: thesis: ex x being Element of ExtREAL st S_{3}[k,x]

end;assume A69: k in Seg 2 ; :: thesis: ex x being Element of ExtREAL st S

per cases
( k = 1 or k = 2 )
by A69, FINSEQ_1:2, TARSKI:def 2;

end;

suppose A70:
k = 1
; :: thesis: ex x being Element of ExtREAL st S_{3}[k,x]

set x = 0. ;

reconsider x = 0. as Element of ExtREAL ;

take x ; :: thesis: S_{3}[k,x]

thus S_{3}[k,x]
by A70; :: thesis: verum

end;reconsider x = 0. as Element of ExtREAL ;

take x ; :: thesis: S

thus S

suppose A71:
k = 2
; :: thesis: ex x being Element of ExtREAL st S_{3}[k,x]

set x = a . (n + 1);

reconsider x = a . (n + 1) as Element of ExtREAL ;

take x ; :: thesis: S_{3}[k,x]

thus S_{3}[k,x]
by A71; :: thesis: verum

end;reconsider x = a . (n + 1) as Element of ExtREAL ;

take x ; :: thesis: S

thus S

A72: ( dom b = Seg 2 & ( for k being Nat st k in Seg 2 holds

S

A73: for k being Nat st k in Seg 2 holds

ex x being Element of S st S

proof

consider G being FinSequence of S such that
let k be Nat; :: thesis: ( k in Seg 2 implies ex x being Element of S st S_{4}[k,x] )

assume A74: k in Seg 2 ; :: thesis: ex x being Element of S st S_{4}[k,x]

end;assume A74: k in Seg 2 ; :: thesis: ex x being Element of S st S

per cases
( k = 1 or k = 2 )
by A74, FINSEQ_1:2, TARSKI:def 2;

end;

suppose A75:
k = 1
; :: thesis: ex x being Element of S st S_{4}[k,x]

set x = union (rng F1);

reconsider x = union (rng F1) as Element of S by MESFUNC2:31;

take x ; :: thesis: S_{4}[k,x]

thus S_{4}[k,x]
by A75; :: thesis: verum

end;reconsider x = union (rng F1) as Element of S by MESFUNC2:31;

take x ; :: thesis: S

thus S

suppose A76:
k = 2
; :: thesis: ex x being Element of S st S_{4}[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: S_{4}[k,x]

thus S_{4}[k,x]
by A76; :: thesis: verum

end;( 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: S

thus S

A77: ( dom G = Seg 2 & ( for k being Nat st k in Seg 2 holds

S

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

len G = 2
by A77, FINSEQ_1:def 3;
let u, v be object ; :: thesis: ( u <> v implies G . u misses G . v )

assume A87: u <> v ; :: thesis: G . u misses G . v

end;assume A87: u <> v ; :: thesis: G . u misses G . v

per cases
( ( u in dom G & v in dom G ) or not u in dom G or not v in dom G )
;

end;

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

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

end;per cases
( ( u = 1 & v = 2 ) or ( u = 2 & v = 1 ) )
by A77, A87, A88, A89, FINSEQ_1:2, TARSKI:def 2;

end;

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

assume
G . u meets G . v
; :: thesis: contradiction

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

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

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

assume
G . u meets G . v
; :: thesis: contradiction

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

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

then A108: G = <*(union (rng F1)),(F . (n + 1))*> by A85, A83, FINSEQ_1:44;

deffunc H

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

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

A122:
for k being Nat st 2 <= k & k in dom b holds
let k be Nat; :: thesis: ( k in dom G implies for v being object st v in G . k holds

f . v = b . k )

assume A120: k in dom G ; :: thesis: for v being object st v in G . k holds

f . v = b . k

let v be object ; :: thesis: ( v in G . k implies f . v = b . k )

assume A121: v in G . k ; :: thesis: f . v = b . k

end;f . v = b . k )

assume A120: k in dom G ; :: thesis: for v being object st v in G . k holds

f . v = b . k

let v be object ; :: thesis: ( v in G . k implies f . v = b . k )

assume A121: v in G . k ; :: thesis: f . v = b . k

( 0. < b . k & b . k < +infty )

proof

dom f =
(union (rng F1)) \/ (F . (n + 1))
by A6, A31, MESFUNC3:def 1
let k be Nat; :: thesis: ( 2 <= k & k in dom b implies ( 0. < b . k & b . k < +infty ) )

assume that

A123: 2 <= k and

A124: k in dom b ; :: thesis: ( 0. < b . k & b . k < +infty )

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: b . k < +infty

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

end;assume that

A123: 2 <= k and

A124: k in dom b ; :: thesis: ( 0. < b . k & b . k < +infty )

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: b . k < +infty

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

.= 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: verum

case A130:
a . (n + 1) = 0.
; :: thesis: integral (M,f) = Sum x

defpred S_{3}[ Nat, set ] means ( ( $1 = 1 implies $2 = 0. ) & ( $1 = 2 implies $2 = 1. ) );

defpred S_{4}[ 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_{4}[k,v]

A135: ( dom G = Seg 2 & ( for k being Nat st k in Seg 2 holds

S_{4}[k,G . k] ) )
from FINSEQ_1:sch 5(A131);

A136: for u, v being object st u <> v holds

G . u misses G . v

ex v being Element of ExtREAL st S_{3}[k,v]

A144: ( dom b = Seg 2 & ( for k being Nat st k in Seg 2 holds

S_{3}[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_{1}( 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_{1}(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

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 )

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

end;defpred S

A131: for k being Nat st k in Seg 2 holds

ex v being Element of S st S

proof

consider G being FinSequence of S such that
let k be Nat; :: thesis: ( k in Seg 2 implies ex v being Element of S st S_{4}[k,v] )

assume A132: k in Seg 2 ; :: thesis: ex v being Element of S st S_{4}[k,v]

end;assume A132: k in Seg 2 ; :: thesis: ex v being Element of S st S

per cases
( k = 1 or k = 2 )
by A132, FINSEQ_1:2, TARSKI:def 2;

end;

suppose A133:
k = 1
; :: thesis: ex v being Element of S st S_{4}[k,v]

set v = union (rng F);

reconsider v = union (rng F) as Element of S by MESFUNC2:31;

take v ; :: thesis: S_{4}[k,v]

thus S_{4}[k,v]
by A133; :: thesis: verum

end;reconsider v = union (rng F) as Element of S by MESFUNC2:31;

take v ; :: thesis: S

thus S

suppose A134:
k = 2
; :: thesis: ex v being Element of S st S_{4}[k,v]

reconsider v = {} as Element of S by PROB_1:4;

take v ; :: thesis: S_{4}[k,v]

thus S_{4}[k,v]
by A134; :: thesis: verum

end;take v ; :: thesis: S

thus S

A135: ( dom G = Seg 2 & ( for k being Nat st k in Seg 2 holds

S

A136: for u, v being object st u <> v holds

G . u misses G . v

proof

A140:
for k being Nat st k in Seg 2 holds
let u, v be object ; :: thesis: ( u <> v implies G . u misses G . v )

assume A137: u <> v ; :: thesis: G . u misses G . v

end;assume A137: u <> v ; :: thesis: G . u misses G . v

per cases
( ( u in dom G & v in dom G ) or not u in dom G or not v in dom G )
;

end;

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

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

end;ex v being Element of ExtREAL st S

proof

consider b being FinSequence of ExtREAL such that
let k be Nat; :: thesis: ( k in Seg 2 implies ex v being Element of ExtREAL st S_{3}[k,v] )

assume A141: k in Seg 2 ; :: thesis: ex v being Element of ExtREAL st S_{3}[k,v]

end;assume A141: k in Seg 2 ; :: thesis: ex v being Element of ExtREAL st S

per cases
( k = 1 or k = 2 )
by A141, FINSEQ_1:2, TARSKI:def 2;

end;

suppose A142:
k = 1
; :: thesis: ex v being Element of ExtREAL st S_{3}[k,v]

set v = 0. ;

reconsider v = 0. as Element of ExtREAL ;

take v ; :: thesis: S_{3}[k,v]

thus S_{3}[k,v]
by A142; :: thesis: verum

end;reconsider v = 0. as Element of ExtREAL ;

take v ; :: thesis: S

thus S

suppose A143:
k = 2
; :: thesis: ex v being Element of ExtREAL st S_{3}[k,v]

set v = 1. ;

reconsider v = 1. as Element of ExtREAL ;

take v ; :: thesis: S_{3}[k,v]

thus S_{3}[k,v]
by A143; :: thesis: verum

end;reconsider v = 1. as Element of ExtREAL ;

take v ; :: thesis: S

thus S

A144: ( dom b = Seg 2 & ( for k being Nat st k in Seg 2 holds

S

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

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

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

len G = 2
by A135, FINSEQ_1:def 3;
let k be Nat; :: thesis: ( k in dom G implies for v being object st v in G . k holds

f . v = b . k )

assume A157: k in dom G ; :: thesis: for v being object st v in G . k holds

f . v = b . k

let v be object ; :: thesis: ( v in G . k implies f . v = b . k )

assume A158: v in G . k ; :: thesis: f . v = b . k

end;f . v = b . k )

assume A157: k in dom G ; :: thesis: for v being object st v in G . k holds

f . v = b . k

let v be object ; :: thesis: ( v in G . k implies f . v = b . k )

assume A158: v in G . k ; :: thesis: f . v = b . k

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

A170:
b . 1 = 0.
by A144, A149;
let k be Nat; :: thesis: ( 2 <= k & k in dom b implies ( 0. < b . k & b . k < +infty ) )

assume that

A167: 2 <= k and

A168: k in dom b ; :: thesis: ( 0. < b . k & b . k < +infty )

( k = 1 or k = 2 ) by A144, A168, FINSEQ_1:2, TARSKI:def 2;

hence 0. < b . k by A144, A165, A167; :: thesis: b . k < +infty

A169: 1 in REAL by NUMBERS:19;

S_{3}[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: verum

end;assume that

A167: 2 <= k and

A168: k in dom b ; :: thesis: ( 0. < b . k & b . k < +infty )

( k = 1 or k = 2 ) by A144, A168, FINSEQ_1:2, TARSKI:def 2;

hence 0. < b . k by A144, A165, A167; :: thesis: b . k < +infty

A169: 1 in REAL by NUMBERS:19;

S

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

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

suppose A172:
dom (f | (union (rng (F | (Seg n))))) <> {}
; :: thesis: integral (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 (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)

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

now :: thesis: ( ( ( F . (n + 1) = {} or a . (n + 1) = 0. ) & integral (M,f) = Sum x ) or ( F . (n + 1) <> {} & a . (n + 1) <> 0. & integral (M,f) = Sum x ) )end;

hence
integral (M,f) = Sum x
; :: thesis: verumper cases
( F . (n + 1) = {} or a . (n + 1) = 0. or ( F . (n + 1) <> {} & a . (n + 1) <> 0. ) )
;

end;

case A187:
( F . (n + 1) = {} or a . (n + 1) = 0. )
; :: thesis: integral (M,f) = Sum x

defpred S_{2}[ 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_{2}[k,x]

A194: ( dom H = Seg (len G) & ( for k being Nat st k in Seg (len G) holds

S_{2}[k,H . k] ) )
from FINSEQ_1:sch 5(A188);

A195: for u, v being object st u <> v holds

H . u misses H . v_{1}( 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_{1}(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)

then A260: n + 1 in dom F by A9, FINSEQ_3:25;

A261: x . (n + 1) = 0.

for x being object st x in H . m holds

f . x = b . m

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

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

end;A188: for k being Nat st k in Seg (len G) holds

ex x being Element of S st S

proof

consider H being FinSequence of S such that
let k be Nat; :: thesis: ( k in Seg (len G) implies ex x being Element of S st S_{2}[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 S_{2}[k,x]

then k in dom G by FINSEQ_1:def 3;

then A190: G . k in rng G by FUNCT_1:3;

end;A189: rng G c= S by FINSEQ_1:def 4;

assume k in Seg (len G) ; :: thesis: ex x being Element of S st S

then k in dom G by FINSEQ_1:def 3;

then A190: G . k in rng G by FUNCT_1:3;

per cases
( k = 1 or k <> 1 )
;

end;

suppose A191:
k = 1
; :: thesis: ex x being Element of S st S_{2}[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;

S_{2}[k,x]
by A191;

hence ex x being Element of S st S_{2}[k,x]
; :: thesis: verum

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

hence ex x being Element of S st S

suppose A193:
k <> 1
; :: thesis: ex x being Element of S st S_{2}[k,x]

set x = G . k;

reconsider x = G . k as Element of S by A190, A189;

S_{2}[k,x]
by A193;

hence ex x being Element of S st S_{2}[k,x]
; :: thesis: verum

end;reconsider x = G . k as Element of S by A190, A189;

S

hence ex x being Element of S st S

A194: ( dom H = Seg (len G) & ( for k being Nat st k in Seg (len G) holds

S

A195: for u, v being object st u <> v holds

H . u misses H . v

proof

deffunc H
let u, v be object ; :: thesis: ( u <> v implies H . u misses H . v )

assume A196: u <> v ; :: thesis: H . u misses H . v

end;assume A196: u <> v ; :: thesis: H . u misses H . v

per cases
( ( u in dom H & v in dom H ) or not u in dom H or not v in dom H )
;

end;

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

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

end;per cases
( u = 1 or u <> 1 )
;

end;

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

hence H . u misses H . v by A200, A201, XBOOLE_1:70; :: thesis: verum

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

( H . u = (G . 1) \/ (F . (n + 1)) & G . 1 misses G . v )
by A194, A196, A197, A198, PROB_2:def 2;per cases
( F . (n + 1) = {} or a . (n + 1) = 0. )
by A187;

end;

suppose A202:
a . (n + 1) = 0.
; :: thesis: F . (n + 1) misses G . v

assume
F . (n + 1) meets G . v
; :: thesis: contradiction

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

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

hence H . u misses H . v by A200, A201, XBOOLE_1:70; :: thesis: verum

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

end;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
( v = 1 or v <> 1 )
;

end;

suppose A211:
v = 1
; :: thesis: H . u misses H . v

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

hence H . u misses H . v by A210, A212, XBOOLE_1:70; :: thesis: verum

end;proof
end;

( H . v = (G . 1) \/ (F . (n + 1)) & G . 1 misses G . u )
by A194, A196, A197, A211, PROB_2:def 2;per cases
( F . (n + 1) = {} or a . (n + 1) = 0. )
by A187;

end;

suppose A213:
a . (n + 1) = 0.
; :: thesis: F . (n + 1) misses G . u

assume
F . (n + 1) meets G . u
; :: thesis: contradiction

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

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

hence H . u misses H . v by A210, A212, XBOOLE_1:70; :: thesis: verum

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

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

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

end;proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in union (rng H) or v in dom f )
let v be object ; :: 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 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;

end;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 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
( u = n + 1 or u <> n + 1 )
;

end;

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

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

end;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
( w = 1 or w <> 1 )
;

end;

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 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
( k = 1 or k <> 1 )
;

end;

suppose
k = 1
; :: thesis: v in dom f

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

end;per cases
( v in G . 1 or v in F . (n + 1) )
by A240, A243, A244, XBOOLE_0:def 3;

end;

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

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

A249: now :: thesis: not -infty in rng x1

1 <= n + 1
by NAT_1:11;assume
-infty in rng x1
; :: thesis: contradiction

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;

end;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
( F . l <> {} or F . l = {} )
;

end;

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

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

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

suppose A259:
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;.= 0. by A259, VALUED_0:def 19 ;

hence contradiction by A253; :: thesis: verum

then A260: n + 1 in dom F by A9, FINSEQ_3:25;

A261: x . (n + 1) = 0.

proof
end;

per cases
( F . (n + 1) = {} or a . (n + 1) = 0. )
by A187;

end;

A265: now :: thesis: not -infty in rng <*(x . (n + 1))*>

A266:
for m being Nat st m in dom H holds 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;then -infty in {(x . (n + 1))} by FINSEQ_1:39;

hence contradiction by A261; :: thesis: verum

for x being object st x in H . m holds

f . x = b . m

proof

A279:
dom z = dom y
by A220, FINSEQ_3:29;
let m be Nat; :: thesis: ( m in dom H implies for x being object st x in H . m holds

f . x = b . m )

assume A267: m in dom H ; :: thesis: for x being object st x in H . m holds

f . x = b . m

let x be object ; :: thesis: ( x in H . m implies f . x = b . m )

assume A268: x in H . m ; :: thesis: f . x = b . m

end;f . x = b . m )

assume A267: m in dom H ; :: thesis: for x being object st x in H . m holds

f . x = b . m

let x be object ; :: thesis: ( x in H . m implies f . x = b . m )

assume A268: x in H . m ; :: thesis: f . x = b . m

per cases
( m = 1 or m <> 1 )
;

end;

suppose A269:
m = 1
; :: thesis: f . x = b . m

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

end;per cases
( x in G . 1 or x in F . (n + 1) )
by A268, A270, XBOOLE_0:def 3;

end;

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

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

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

len x = n + 1
by A7, A9, FINSEQ_3:29;
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;

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

per cases
( k = 1 or k <> 1 )
;

end;

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

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

case A290:
( F . (n + 1) <> {} & a . (n + 1) <> 0. )
; :: thesis: integral (M,f) = Sum x

defpred S_{2}[ 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_{2}[k,v]

A296: ( dom c = Seg ((len b) + 1) & ( for k being Nat st k in Seg ((len b) + 1) holds

S_{2}[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 )

_{3}[ 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_{3}[k,v]

A343: ( dom H = Seg ((len G) + 1) & ( for k being Nat st k in Seg ((len G) + 1) holds

S_{3}[k,H . k] ) )
from FINSEQ_1:sch 5(A337);

A344: for i, j being object st i <> j holds

H . i misses H . j

A370: Seg (len H) = Seg ((len G) + 1) by A343, FINSEQ_1:def 3;

defpred S_{4}[ 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_{4}[k,v]

A374: ( dom z = Seg ((len y) + 1) & ( for k being Nat st k in Seg ((len y) + 1) holds

S_{4}[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)

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

.= 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 <> {}

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

.= (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

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

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

proof

consider c being FinSequence of ExtREAL such that
let k be Nat; :: thesis: ( k in Seg ((len b) + 1) implies ex v being Element of ExtREAL st S_{2}[k,v] )

assume k in Seg ((len b) + 1) ; :: thesis: ex v being Element of ExtREAL st S_{2}[k,v]

end;assume k in Seg ((len b) + 1) ; :: thesis: ex v being Element of ExtREAL st S

per cases
( k <> (len b) + 1 or k = (len b) + 1 )
;

end;

suppose A294:
k <> (len b) + 1
; :: thesis: ex v being Element of ExtREAL st S_{2}[k,v]

reconsider v = b . k as Element of ExtREAL ;

take v ; :: thesis: S_{2}[k,v]

thus S_{2}[k,v]
by A294; :: thesis: verum

end;take v ; :: thesis: S

thus S

suppose A295:
k = (len b) + 1
; :: thesis: ex v being Element of ExtREAL st S_{2}[k,v]

reconsider v = a . (n + 1) as Element of ExtREAL ;

take v ; :: thesis: S_{2}[k,v]

thus S_{2}[k,v]
by A295, NAT_1:13; :: thesis: verum

end;take v ; :: thesis: S

thus S

A296: ( dom c = Seg ((len b) + 1) & ( for k being Nat st k in Seg ((len b) + 1) holds

S

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

A309:
0. <= a . (n + 1)
by A6, A297, A292, A301, MESFUNC3:def 1;
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;

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

per cases
( m = len c or m <> len c )
;

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

A310: now :: thesis: ( not -infty in rng y & not -infty in rng <*((a . (n + 1)) * ((M * F) . (n + 1)))*> )

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

end;per cases
( -infty in rng y or -infty in rng <*((a . (n + 1)) * ((M * F) . (n + 1)))*> )
by A311;

end;

suppose
-infty in rng y
; :: thesis: contradiction

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;

end;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
( k = 1 or k <> 1 )
;

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

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

proof

defpred S
reconsider EMPTY = {} as Element of S by PROB_1:4;

assume -infty in rng x1 ; :: thesis: contradiction

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;

end;assume -infty in rng x1 ; :: thesis: contradiction

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
( F . k <> {} or F . k = {} )
;

end;

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

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

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

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;.= (M * F) . k by A7, A327, FUNCT_1:13 ;

hence contradiction by A325, A326, A328, FUNCT_1:47; :: thesis: verum

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

proof

consider H being FinSequence of S such that
let k be Nat; :: thesis: ( k in Seg ((len G) + 1) implies ex v being Element of S st S_{3}[k,v] )

assume A338: k in Seg ((len G) + 1) ; :: thesis: ex v being Element of S st S_{3}[k,v]

end;assume A338: k in Seg ((len G) + 1) ; :: thesis: ex v being Element of S st S

per cases
( k <> (len G) + 1 or k = (len G) + 1 )
;

end;

suppose A339:
k <> (len G) + 1
; :: thesis: ex v being Element of S st S_{3}[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: S_{3}[k,v]

thus S_{3}[k,v]
by A339; :: thesis: verum

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

thus S

suppose A342:
k = (len G) + 1
; :: thesis: ex v being Element of S st S_{3}[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: S_{3}[k,v]

thus S_{3}[k,v]
by A342, NAT_1:13; :: thesis: verum

end;then reconsider v = F . (n + 1) as Element of S ;

take v ; :: thesis: S

thus S

A343: ( dom H = Seg ((len G) + 1) & ( for k being Nat st k in Seg ((len G) + 1) holds

S

A344: for i, j being object st i <> j holds

H . i misses H . j

proof

A369:
len H = (len G) + 1
by A343, FINSEQ_1:def 3;
let i, j be object ; :: thesis: ( i <> j implies H . i misses H . j )

assume A345: i <> j ; :: thesis: H . i misses H . j

end;assume A345: i <> j ; :: thesis: H . i misses H . j

per cases
( ( i in dom H & j in dom H ) or not i in dom H or not j in dom H )
;

end;

suppose A346:
( 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)

A362: i <= (len G) + 1 by A343, A346, FINSEQ_1:1;

A363: S_{3}[i,H . i]
by A343, A346;

A364: S_{3}[j,H . j]
by A343, A346;

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

A361:
1 <= j
by A343, A346, FINSEQ_1:1;
A350:
union (rng F1) 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;proof

let k be Nat; :: thesis: ( 1 <= k & k <= len G implies H . k misses F . (n + 1) )
assume
union (rng F1) meets F . (n + 1)
; :: thesis: contradiction

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

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

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

A362: i <= (len G) + 1 by A343, A346, FINSEQ_1:1;

A363: S

A364: S

per cases
( i = (len G) + 1 or i <> (len G) + 1 )
;

end;

suppose A365:
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;then j <= len G by NAT_1:13;

hence H . i misses H . j by A361, A363, A349, A365; :: thesis: verum

A370: Seg (len H) = Seg ((len G) + 1) by A343, FINSEQ_1:def 3;

defpred S

A371: for k being Nat st k in Seg ((len y) + 1) holds

ex v being Element of ExtREAL st S

proof

consider z being FinSequence of ExtREAL such that
let k be Nat; :: thesis: ( k in Seg ((len y) + 1) implies ex v being Element of ExtREAL st S_{4}[k,v] )

assume k in Seg ((len y) + 1) ; :: thesis: ex v being Element of ExtREAL st S_{4}[k,v]

end;assume k in Seg ((len y) + 1) ; :: thesis: ex v being Element of ExtREAL st S

A374: ( dom z = Seg ((len y) + 1) & ( for k being Nat st k in Seg ((len y) + 1) holds

S

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

reconsider H = H as Finite_Sep_Sequence of S by A344, PROB_2:def 2;
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: S_{2}[m,c . m]
by A296, A336, A374, A375;

end;assume A381: m in dom z ; :: thesis: z . m = (c . m) * ((M * H) . m)

then A382: S

per cases
( m = (len y) + 1 or m <> (len y) + 1 )
;

end;

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

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

len (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) =
(len y) + 1
by FINSEQ_2:16
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

end;assume that

A389: 1 <= k and

A390: k <= len z ; :: thesis: z . k = (y ^ <*((a . (n + 1)) * ((M * F) . (n + 1)))*>) . k

per cases
( k = len z or k <> len z )
;

end;

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

.= 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

then
b <> {}
by A177, MESFUNC3:def 1, RELAT_1:38;
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 {} = 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

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

len H =
(len G) + 1
by A343, FINSEQ_1:def 3
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: S_{3}[k,H . k]
by A343;

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

.= (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

then A418:
H,c are_Re-presentation_of f
by A343, A296, A336, A405, MESFUNC3:def 1;
let m be Nat; :: thesis: ( m in dom H implies for v being object st v in H . m holds

f . v = c . m )

assume A406: m in dom H ; :: thesis: for v being object st v in H . m holds

f . v = c . m

then A407: S_{3}[m,H . m]
by A343;

A408: m <= (len G) + 1 by A343, A406, FINSEQ_1:1;

let v be object ; :: thesis: ( v in H . m implies f . v = c . m )

assume A409: v in H . m ; :: thesis: f . v = c . m

A410: S_{2}[m,c . m]
by A343, A296, A336, A406;

A411: 1 <= m by A343, A406, FINSEQ_1:1;

end;f . v = c . m )

assume A406: m in dom H ; :: thesis: for v being object st v in H . m holds

f . v = c . m

then A407: S

A408: m <= (len G) + 1 by A343, A406, FINSEQ_1:1;

let v be object ; :: thesis: ( v in H . m implies f . v = c . m )

assume A409: v in H . m ; :: thesis: f . v = c . m

A410: S

A411: 1 <= m by A343, A406, FINSEQ_1:1;

per cases
( m = (len G) + 1 or m <> (len G) + 1 )
;

end;

suppose A412:
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;hence f . v = c . m by A6, A335, A407, A410, A409, A412, FINSEQ_1:6, MESFUNC3:def 1; :: thesis: verum

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

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

proof

for n being Nat holds S
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 <> {} & 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 = 0 holds

integral (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 <> {} & 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 = 0 holds

integral (M,f) = Sum x

let a, x be FinSequence of ExtREAL ; :: thesis: ( 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 = 0 implies integral (M,f) = Sum x )

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: integral (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 (M,f) = Sum x by A420, A421, MESFUNC3:def 1; :: thesis: verum

end;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 = 0 holds

integral (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 <> {} & 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 = 0 holds

integral (M,f) = Sum x

let a, x be FinSequence of ExtREAL ; :: thesis: ( 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 = 0 implies integral (M,f) = Sum x )

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: integral (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 (M,f) = Sum x by A420, A421, MESFUNC3:def 1; :: thesis: verum

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