let a, b be Real; :: thesis: for A being non empty closed_interval Subset of REAL

for D being Division of A

for f being PartFunc of A,REAL st A = [.a,b.] holds

ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )

let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A

for f being PartFunc of A,REAL st A = [.a,b.] holds

ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )

let D be Division of A; :: thesis: for f being PartFunc of A,REAL st A = [.a,b.] holds

ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )

let f be PartFunc of A,REAL; :: thesis: ( A = [.a,b.] implies ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) ) )

assume A = [.a,b.] ; :: thesis: ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )

then consider F being Finite_Sep_Sequence of Borel_Sets such that

A1: dom F = dom D and

A2: union (rng F) = A and

A3: for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) by Th9;

defpred S_{1}[ object , object ] means ex k being Nat st

( 1 <= k & k <= len F & $1 in F . k & $2 = upper_bound (rng (f | (divset (D,k)))) );

A4: for x, y being object st x in REAL & S_{1}[x,y] holds

y in ExtREAL by XXREAL_0:def 1;

A5: for x, y1, y2 being object st x in REAL & S_{1}[x,y1] & S_{1}[x,y2] holds

y1 = y2 by PROB_2:def 2, XBOOLE_0:3;

consider g being PartFunc of REAL,ExtREAL such that

A6: for x being object holds

( x in dom g iff ( x in REAL & ex y being object st S_{1}[x,y] ) )
and

A7: for x being object st x in dom g holds

S_{1}[x,g . x]
from PARTFUN1:sch 2(A4, A5);

then A9: g is V55() by VALUED_0:def 3;

then A18: dom g = union (rng F) by A13, XBOOLE_0:def 10;

A19: for k being Nat

for x, y being Element of REAL st k in dom F & x in F . k & y in F . k holds

g . x = g . y

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) by A7;

hence ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) ) by A1, A3, A2, A18, A19, A9, MESFUNC2:def 4; :: thesis: verum

for D being Division of A

for f being PartFunc of A,REAL st A = [.a,b.] holds

ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )

let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A

for f being PartFunc of A,REAL st A = [.a,b.] holds

ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )

let D be Division of A; :: thesis: for f being PartFunc of A,REAL st A = [.a,b.] holds

ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )

let f be PartFunc of A,REAL; :: thesis: ( A = [.a,b.] implies ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) ) )

assume A = [.a,b.] ; :: thesis: ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) )

then consider F being Finite_Sep_Sequence of Borel_Sets such that

A1: dom F = dom D and

A2: union (rng F) = A and

A3: for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) by Th9;

defpred S

( 1 <= k & k <= len F & $1 in F . k & $2 = upper_bound (rng (f | (divset (D,k)))) );

A4: for x, y being object st x in REAL & S

y in ExtREAL by XXREAL_0:def 1;

A5: for x, y1, y2 being object st x in REAL & S

y1 = y2 by PROB_2:def 2, XBOOLE_0:3;

consider g being PartFunc of REAL,ExtREAL such that

A6: for x being object holds

( x in dom g iff ( x in REAL & ex y being object st S

A7: for x being object st x in dom g holds

S

now :: thesis: for y being object st y in rng g holds

y in REAL

then
rng g c= REAL
;y in REAL

let y be object ; :: thesis: ( y in rng g implies y in REAL )

assume y in rng g ; :: thesis: y in REAL

then consider x being Element of REAL such that

A8: ( x in dom g & y = g . x ) by PARTFUN1:3;

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) by A7, A8;

hence y in REAL by A8, XREAL_0:def 1; :: thesis: verum

end;assume y in rng g ; :: thesis: y in REAL

then consider x being Element of REAL such that

A8: ( x in dom g & y = g . x ) by PARTFUN1:3;

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) by A7, A8;

hence y in REAL by A8, XREAL_0:def 1; :: thesis: verum

then A9: g is V55() by VALUED_0:def 3;

now :: thesis: for x being object st x in dom g holds

x in union (rng F)

then A13:
dom g c= union (rng F)
;x in union (rng F)

let x be object ; :: thesis: ( x in dom g implies x in union (rng F) )

assume x in dom g ; :: thesis: x in union (rng F)

then consider y being object such that

A10: ex k being Nat st

( 1 <= k & k <= len F & x in F . k & y = upper_bound (rng (f | (divset (D,k)))) ) by A6;

consider k being Nat such that

A11: ( 1 <= k & k <= len F ) and

A12: x in F . k and

y = upper_bound (rng (f | (divset (D,k)))) by A10;

k in dom F by A11, FINSEQ_3:25;

then F . k in rng F by FUNCT_1:3;

hence x in union (rng F) by A12, TARSKI:def 4; :: thesis: verum

end;assume x in dom g ; :: thesis: x in union (rng F)

then consider y being object such that

A10: ex k being Nat st

( 1 <= k & k <= len F & x in F . k & y = upper_bound (rng (f | (divset (D,k)))) ) by A6;

consider k being Nat such that

A11: ( 1 <= k & k <= len F ) and

A12: x in F . k and

y = upper_bound (rng (f | (divset (D,k)))) by A10;

k in dom F by A11, FINSEQ_3:25;

then F . k in rng F by FUNCT_1:3;

hence x in union (rng F) by A12, TARSKI:def 4; :: thesis: verum

now :: thesis: for x being object st x in union (rng F) holds

x in dom g

then
union (rng F) c= dom g
;x in dom g

let x be object ; :: thesis: ( x in union (rng F) implies x in dom g )

assume A14: x in union (rng F) ; :: thesis: x in dom g

then consider P being set such that

A15: ( x in P & P in rng F ) by TARSKI:def 4;

consider k being Element of NAT such that

A16: ( k in dom F & P = F . k ) by A15, PARTFUN1:3;

A17: ( 1 <= k & k <= len F ) by A16, FINSEQ_3:25;

upper_bound (rng (f | (divset (D,k)))) in REAL by XREAL_0:def 1;

hence x in dom g by A6, A14, A2, A15, A16, A17; :: thesis: verum

end;assume A14: x in union (rng F) ; :: thesis: x in dom g

then consider P being set such that

A15: ( x in P & P in rng F ) by TARSKI:def 4;

consider k being Element of NAT such that

A16: ( k in dom F & P = F . k ) by A15, PARTFUN1:3;

A17: ( 1 <= k & k <= len F ) by A16, FINSEQ_3:25;

upper_bound (rng (f | (divset (D,k)))) in REAL by XREAL_0:def 1;

hence x in dom g by A6, A14, A2, A15, A16, A17; :: thesis: verum

then A18: dom g = union (rng F) by A13, XBOOLE_0:def 10;

A19: for k being Nat

for x, y being Element of REAL st k in dom F & x in F . k & y in F . k holds

g . x = g . y

proof

for x being Real st x in dom g holds
let k be Nat; :: thesis: for x, y being Element of REAL st k in dom F & x in F . k & y in F . k holds

g . x = g . y

let x, y be Element of REAL ; :: thesis: ( k in dom F & x in F . k & y in F . k implies g . x = g . y )

assume that

A20: k in dom F and

A21: x in F . k and

A22: y in F . k ; :: thesis: g . x = g . y

F . k in rng F by A20, FUNCT_1:3;

then A23: ( x in dom g & y in dom g ) by A18, A21, A22, TARSKI:def 4;

then consider k1 being Nat such that

( 1 <= k1 & k1 <= len F ) and

A24: x in F . k1 and

A25: g . x = upper_bound (rng (f | (divset (D,k1)))) by A7;

consider k2 being Nat such that

( 1 <= k2 & k2 <= len F ) and

A26: y in F . k2 and

A27: g . y = upper_bound (rng (f | (divset (D,k2)))) by A23, A7;

( k = k1 & k = k2 ) by A21, A22, A24, A26, XBOOLE_0:3, PROB_2:def 2;

hence g . x = g . y by A25, A27; :: thesis: verum

end;g . x = g . y

let x, y be Element of REAL ; :: thesis: ( k in dom F & x in F . k & y in F . k implies g . x = g . y )

assume that

A20: k in dom F and

A21: x in F . k and

A22: y in F . k ; :: thesis: g . x = g . y

F . k in rng F by A20, FUNCT_1:3;

then A23: ( x in dom g & y in dom g ) by A18, A21, A22, TARSKI:def 4;

then consider k1 being Nat such that

( 1 <= k1 & k1 <= len F ) and

A24: x in F . k1 and

A25: g . x = upper_bound (rng (f | (divset (D,k1)))) by A7;

consider k2 being Nat such that

( 1 <= k2 & k2 <= len F ) and

A26: y in F . k2 and

A27: g . y = upper_bound (rng (f | (divset (D,k2)))) by A23, A7;

( k = k1 & k = k2 ) by A21, A22, A24, A26, XBOOLE_0:3, PROB_2:def 2;

hence g . x = g . y by A25, A27; :: thesis: verum

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) by A7;

hence ex F being Finite_Sep_Sequence of Borel_Sets ex g being PartFunc of REAL,ExtREAL st

( dom F = dom D & union (rng F) = A & ( for k being Nat st k in dom F holds

( ( len D = 1 implies F . k = [.a,b.] ) & ( len D <> 1 implies ( ( k = 1 implies F . k = [.a,(D . k).[ ) & ( 1 < k & k < len D implies F . k = [.(D . (k -' 1)),(D . k).[ ) & ( k = len D implies F . k = [.(D . (k -' 1)),(D . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & dom g = A & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len F & x in F . k & g . x = upper_bound (rng (f | (divset (D,k)))) ) ) ) by A1, A3, A2, A18, A19, A9, MESFUNC2:def 4; :: thesis: verum