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 = lower_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 = lower_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 = lower_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 = lower_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 = lower_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₁[ object , object ] means ex k being Nat st
( 1 <= k & k <= len F & $1 in F . k & $2 = lower_bound (rng (f | (divset (D,k)))) );
A4: for x, y being object st x in REAL & S₁[x,y] holds
y in ExtREAL by XXREAL_0:def 1;
A5: for x, y1, y2 being object st x in REAL & S₁[x,y1] & S₁[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₁[x,y] ) ) and
A7: for x being object st x in dom g holds
S₁[x,g . x] from PARTFUN1:sch 2(A4, A5);

now :: thesis: for y being object st y in rng g holds
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 = lower_bound (rng (f | (divset (D,k)))) ) by A7, A8;
hence y in REAL by A8, XREAL_0:def 1; :: thesis: verum

end;

then rng g c= REAL ;
then A9: g is real-valued by VALUED_0:def 3;

now :: thesis: for x being object st x in dom g holds
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 = lower_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 = lower_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;

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

now :: thesis: for x being object st x in union (rng F) holds
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;
lower_bound (rng (f | (divset (D,k)))) in REAL by XREAL_0:def 1;
hence x in dom g by A6, A15, A16, A14, A2, A17; :: thesis: verum

end;

then union (rng F) c= dom g ;
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

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

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 = lower_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 = lower_bound (rng (f | (divset (D,k)))) ) ) ) by A1, A3, A2, A18, A19, A9, MESFUNC2:def 4; :: thesis: verum