let a, b be Real; 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; 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; 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; ( 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.]
; 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 S1[ 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 & S1[x,y] holds
y in ExtREAL
by XXREAL_0:def 1;
A5:
for x, y1, y2 being object st x in REAL & S1[x,y1] & S1[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 S1[x,y] ) )
and
A7:
for x being object st x in dom g holds
S1[x,g . x]
from PARTFUN1:sch 2(A4, A5);
then
rng g c= REAL
;
then A9:
g is V55()
by VALUED_0:def 3;
then A13:
dom g c= union (rng F)
;
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;
for x, y being Element of REAL st k in dom F & x in F . k & y in F . k holds
g . x = g . ylet x,
y be
Element of
REAL ;
( 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
;
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;
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; verum