let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
assume that
A1: ex A being Element of S st
( A = dom f & f is A -measurable ) and
A2: f is nonnegative ; :: thesis:
defpred S₁[ Element of NAT , PartFunc of X,ExtREAL] means ( dom $2 = dom f & ( for x being Element of X st x in dom f holds
( ( for k being Nat st 1 <= k & k <= (2 |^ $1) * $1 & (k - 1) / (2 |^ $1) <= f . x & f . x < k / (2 |^ $1) holds
$2 . x = (k - 1) / (2 |^ $1) ) & ( $1 <= f . x implies $2 . x = $1 ) ) ) );
A3: for n being Element of NAT ex y being Element of PFuncs (X,ExtREAL) st S₁[n,y]

proof

let n be Element of NAT ; :: thesis:
reconsider nn = n as Nat ;
defpred S₂[ object , object ] means ( ( for k being Nat st 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= f . $1 & f . $1 < k / (2 |^ n) holds
$2 = (k - 1) / (2 |^ n) ) & ( n <= f . $1 implies $2 = n ) );
A4: for x being object st x in dom f holds
ex y being object st S₂[x,y]

proof

let x be object ; :: thesis:
assume x in dom f ; :: thesis:

per cases ;

suppose A5: f . x < n ; :: thesis:

0 <= f . x by A2, SUPINF_2:51;
then consider k being Nat such that
1 <= k and
k <= (2 |^ nn) * nn and
A6: (k - 1) / (2 |^ nn) <= f . x and
A7: f . x < k / (2 |^ nn) by A5, Th4;
take y = (k - 1) / (2 |^ n); :: thesis:

now :: thesis:

let k1 be Nat; :: thesis:
assume that
1 <= k1 and
k1 <= (2 |^ n) * n and
A8: (k1 - 1) / (2 |^ n) <= f . x and
A9: f . x < k1 / (2 |^ n) ; :: thesis:

A10: now :: thesis:

assume k1 < k ; :: thesis:
then k1 + 1 <= k by NAT_1:13;
then k1 <= k - 1 by XREAL_1:19;
then k1 / (2 |^ n) <= (k - 1) / (2 |^ n) by XREAL_1:72;
hence contradiction by A6, A9, XXREAL_0:2; :: thesis:

end;

now :: thesis:

assume k < k1 ; :: thesis:
then k + 1 <= k1 by NAT_1:13;
then k <= k1 - 1 by XREAL_1:19;
then k / (2 |^ n) <= (k1 - 1) / (2 |^ n) by XREAL_1:72;
hence contradiction by A7, A8, XXREAL_0:2; :: thesis:

end;

hence y = (k1 - 1) / (2 |^ n) by A10, XXREAL_0:1; :: thesis:

end;

hence S₂[x,y] by A5; :: thesis:

end;

suppose A11: n <= f . x ; :: thesis:

reconsider y = nn as Real ;
take y ; :: thesis:
thus for k being Nat st 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= f . x & f . x < k / (2 |^ n) holds
y = (k - 1) / (2 |^ n) :: thesis:

proof

let k be Nat; :: thesis:
assume that
1 <= k and
A12: k <= (2 |^ n) * n and
(k - 1) / (2 |^ n) <= f . x and
A13: f . x < k / (2 |^ n) ; :: thesis:
reconsider p = f . x as ExtReal ;
k <= (2 |^ nn) * nn by A12;
then k / (2 |^ nn) <= p by A11, Th5;
then k / (2 |^ n) <= p ;
hence y = (k - 1) / (2 |^ n) by A13; :: thesis:

end;

thus ( n <= f . x implies y = n ) ; :: thesis:

end;

end;

end;

consider fn being Function such that
A14: ( dom fn = dom f & ( for x being object st x in dom f holds
S₂[x,fn . x] ) ) from CLASSES1:sch 1(A4);

now :: thesis:

let w be object ; :: thesis:
assume w in rng fn ; :: thesis:
then consider v being object such that
A15: v in dom fn and
A16: w = fn . v by FUNCT_1:def 3;

per cases ;

suppose n <= f . v ; :: thesis:

then fn . v = n by A14, A15;
hence w in ExtREAL by A16, XXREAL_0:def 1; :: thesis:

end;

suppose A17: f . v < n ; :: thesis:

0 <= f . v by A2, SUPINF_2:51;
then consider k being Nat such that
A18: 1 <= k and
A19: k <= (2 |^ nn) * nn and
A20: (k - 1) / (2 |^ nn) <= f . v and
A21: f . v < k / (2 |^ nn) by A17, Th4;
fn . v = (k - 1) / (2 |^ n) by A14, A15, A18, A19, A20, A21;
hence w in ExtREAL by A16; :: thesis:

end;

end;

end;

then rng fn c= ExtREAL ;
then reconsider fn = fn as PartFunc of (dom f),ExtREAL by A14, RELSET_1:4;
reconsider fn = fn as PartFunc of X,ExtREAL by A14, RELSET_1:5;
reconsider y = fn as Element of PFuncs (X,ExtREAL) by PARTFUN1:45;
take y ; :: thesis:
thus S₁[n,y] by A14; :: thesis:

end;

consider F being sequence of (PFuncs (X,ExtREAL)) such that
A22: for n being Element of NAT holds S₁[n,F . n] from FUNCT_2:sch 3(A3);
A23: for n being Element of NAT holds dom (F . n) = dom f by A22;
A24: for n being Element of NAT
for x being Element of X st x in dom f holds
( ( for k being Nat st 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= f . x & f . x < k / (2 |^ n) holds
(F . n) . x = (k - 1) / (2 |^ n) ) & ( n <= f . x implies (F . n) . x = n ) ) by A22;

A25: now :: thesis:

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
hence dom (F . n) = dom f by A23; :: thesis:

end;

reconsider F = F as Functional_Sequence of X,ExtREAL ;
consider A being Element of S such that
A26: A = dom f and
A27: f is A -measurable by A1;
A28: for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x

proof

let n, m be Nat; :: thesis:
assume A29: n <= m ; :: thesis:
reconsider nn = n, mm = m as Element of NAT by ORDINAL1:def 12;
let x be Element of X; :: thesis:
assume A30: x in dom f ; :: thesis:

per cases ;

suppose A31: m <= f . x ; :: thesis:

then A32: nn <= f . x by A29, XXREAL_0:2;
(F . mm) . x = m by A24, A30, A31;
hence (F . n) . x <= (F . m) . x by A24, A29, A30, A32; :: thesis:

end;

suppose A33: f . x < m ; :: thesis:

A34: 0 <= f . x by A2, SUPINF_2:51;
then consider M being Nat such that
A35: 1 <= M and
A36: M <= (2 |^ m) * m and
A37: (M - 1) / (2 |^ m) <= f . x and
A38: f . x < M / (2 |^ m) by A33, Th4;
reconsider M = M as Element of NAT by ORDINAL1:def 12;
A39: (F . mm) . x = (M - 1) / (2 |^ m) by A24, A30, A35, A36, A37, A38;

per cases ;

suppose A40: n <= f . x ; :: thesis:

reconsider M1 = 2 |^ mm as Element of NAT ;
n < M / (2 |^ m) by A38, A40, XXREAL_0:2;
then (2 |^ m) * n < M by PREPOWER:6, XREAL_1:79;
then (M1 * n) + 1 <= M by NAT_1:13;
then A41: M1 * n <= M - 1 by XREAL_1:19;
A42: 0 < 2 |^ m by PREPOWER:6;
(F . n) . x = nn by A24, A30, A40;
hence (F . n) . x <= (F . m) . x by A39, A42, A41, XREAL_1:77; :: thesis:

end;

suppose A43: f . x < n ; :: thesis:

consider k being Nat such that
A44: m = nn + k by A29, NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
reconsider K = 2 |^ k as Element of NAT ;
consider N1 being Nat such that
A45: 1 <= N1 and
A46: N1 <= (2 |^ n) * n and
A47: (N1 - 1) / (2 |^ n) <= f . x and
A48: f . x < N1 / (2 |^ n) by A34, A43, Th4;
reconsider N1 = N1 as Element of NAT by ORDINAL1:def 12;
A49: (F . nn) . x = (N1 - 1) / (2 |^ nn) by A24, A30, A45, A46, A47, A48;
(N1 - 1) / (2 |^ n) < M / (2 |^ (n + k)) by A38, A47, A44, XXREAL_0:2;
then (N1 - 1) / (2 |^ n) < M / ((2 |^ n) * (2 |^ k)) by NEWTON:8;
then (N1 - 1) / (2 |^ n) < (M / (2 |^ k)) / (2 |^ n) by XCMPLX_1:78;
then N1 - 1 < M / (2 |^ k) by XREAL_1:72;
then K * (N1 - 1) < M by PREPOWER:6, XREAL_1:79;
then (K * (N1 - 1)) + 1 <= M by INT_1:7;
then K * (N1 - 1) <= M - 1 by XREAL_1:19;
then (K * (N1 - 1)) / (2 |^ (n + k)) <= (M - 1) / (2 |^ (n + k)) by XREAL_1:72;
then A50: (K * (N1 - 1)) / ((2 |^ n) * (2 |^ k)) <= (M - 1) / (2 |^ (n + k)) by NEWTON:8;
2 |^ k > 0 by PREPOWER:6;
hence (F . n) . x <= (F . m) . x by A39, A49, A44, A50, XCMPLX_1:91; :: thesis:

end;

end;

end;

end;

end;

A51: for n being Nat holds F . n is_simple_func_in S

proof

let n be Nat; :: thesis:
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
reconsider N = 2 |^ nn as Element of NAT ;
defpred S₂[ Nat, set ] means ( ( $1 <= N * n implies $2 = (A /\ (great_eq_dom (f,(($1 - 1) / (2 |^ n))))) /\ (less_dom (f,($1 / (2 |^ n)))) ) & ( $1 = (N * n) + 1 implies $2 = A /\ (great_eq_dom (f,n)) ) );

now :: thesis:

let x be Element of X; :: thesis:
assume x in dom (F . n) ; :: thesis:
then A52: x in dom f by A25;

per cases ;

suppose A53: n <= f . x ; :: thesis:

then (F . nn) . x = n by A24, A52;
then (F . n) . x in REAL by XREAL_0:def 1;
then A54: (F . n) . x < +infty by XXREAL_0:9;
- +infty < (F . nn) . x by A24, A52, A53;
hence |.((F . n) . x).| < +infty by A54, EXTREAL1:22; :: thesis:

end;

suppose A55: f . x < n ; :: thesis:

A56: 0 <= f . x by A2, SUPINF_2:51;
nn in REAL by XREAL_0:def 1;
then nn < +infty by XXREAL_0:9;
then reconsider y = f . x as Element of REAL by A55, A56, XXREAL_0:14;
set k = [\((2 |^ n) * y)/] + 1;
A57: [\((2 |^ n) * y)/] <= (2 |^ n) * y by INT_1:def 6;
((2 |^ n) * y) - 1 < [\((2 |^ n) * y)/] by INT_1:def 6;
then A58: (2 |^ n) * y < [\((2 |^ n) * y)/] + 1 by XREAL_1:19;
A59: 0 < 2 |^ n by PREPOWER:6;
then (2 |^ n) * y < (2 |^ n) * n by A55, XREAL_1:68;
then [\((2 |^ n) * y)/] < (2 |^ n) * n by A57, XXREAL_0:2;
then A60: [\((2 |^ n) * y)/] + 1 <= (2 |^ n) * n by INT_1:7;
A61: 0 <= (2 |^ n) * y by A56;
then A62: 0 + 1 <= [\((2 |^ n) * y)/] + 1 by A58, INT_1:7;
reconsider k = [\((2 |^ n) * y)/] + 1 as Element of NAT by A61, A58, INT_1:3;
reconsider k = k as Nat ;
k - 1 <= (2 |^ n) * y by INT_1:def 6;
then A63: (k - 1) / (2 |^ nn) <= y by PREPOWER:6, XREAL_1:79;
A64: (k - 1) / (2 |^ nn) in REAL by XREAL_0:def 1;
y < k / (2 |^ nn) by A59, INT_1:29, XREAL_1:81;
then A65: (F . nn) . x = (k - 1) / (2 |^ nn) by A24, A52, A62, A60, A63;
then -infty < (F . n) . x by XXREAL_0:12, A64;
then A66: - +infty < (F . n) . x by XXREAL_3:def 3;
(F . n) . x < +infty by A65, XXREAL_0:9, A64;
hence |.((F . n) . x).| < +infty by A66, EXTREAL1:22; :: thesis:

end;

end;

end;

then A67: F . n is real-valued by MESFUNC2:def 1;

A68: now :: thesis:

let k be Nat; :: thesis:
assume k in Seg ((N * n) + 1) ; :: thesis:
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

per cases ;

suppose A69: k <> (N * n) + 1 ; :: thesis:

set B = (A /\ (great_eq_dom (f,((k1 - 1) / (2 |^ n))))) /\ (less_dom (f,(k1 / (2 |^ n))));
reconsider B = (A /\ (great_eq_dom (f,((k1 - 1) / (2 |^ n))))) /\ (less_dom (f,(k1 / (2 |^ n)))) as Element of S by A26, A27, Th33;
take B = B; :: thesis:
thus S₂[k,B] by A69; :: thesis:

end;

suppose A70: k = (N * n) + 1 ; :: thesis:

set B = A /\ (great_eq_dom (f,n));
reconsider B = A /\ (great_eq_dom (f,n)) as Element of S by A26, A27, MESFUNC1:27;
take B = B; :: thesis:
thus S₂[k,B] by A70, NAT_1:13; :: thesis:

end;

end;

end;

consider G being FinSequence of S such that
A71: ( dom G = Seg ((N * n) + 1) & ( for k being Nat st k in Seg ((N * n) + 1) holds
S₂[k,G . k] ) ) from FINSEQ_1:sch 5(A68);

A72: now :: thesis:

let k be Nat; :: thesis:
assume that
A73: 1 <= k and
A74: k <= (2 |^ n) * n ; :: thesis:
k <= (N * n) + 1 by A74, NAT_1:12;
then k in Seg ((N * n) + 1) by A73;
hence G . k = (A /\ (great_eq_dom (f,((k - 1) / (2 |^ n))))) /\ (less_dom (f,(k / (2 |^ n)))) by A71, A74; :: thesis:

end;

A75: len G = ((2 |^ n) * n) + 1 by A71, FINSEQ_1:def 3;

now :: thesis:

let x, y be object ; :: thesis:
assume A76: x <> y ; :: thesis:

per cases ;

suppose ( not x in dom G or not y in dom G ) ; :: thesis:

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

end;

suppose A77: ( x in dom G & y in dom G ) ; :: thesis:

then reconsider x1 = x, y1 = y as Nat ;
A78: x1 in Seg (len G) by A77, FINSEQ_1:def 3;
then A79: 1 <= x1 by FINSEQ_1:1;
A80: y1 in Seg (len G) by A77, FINSEQ_1:def 3;
then A81: 1 <= y1 by FINSEQ_1:1;
A82: y1 <= ((2 |^ n) * n) + 1 by A75, A80, FINSEQ_1:1;
A83: x1 <= ((2 |^ n) * n) + 1 by A75, A78, FINSEQ_1:1;

now :: thesis:

per cases by A76, XXREAL_0:1;

case A84: x1 < y1 ; :: thesis:

hereby :: thesis:

assume A85: y1 = ((2 |^ n) * n) + 1 ; :: thesis:
then A86: G . y = A /\ (great_eq_dom (f,n)) by A71, A77;
A87: x1 <= N * n by A84, A85, NAT_1:13;
then A88: G . x = (A /\ (great_eq_dom (f,((x1 - 1) / (2 |^ n))))) /\ (less_dom (f,(x1 / (2 |^ n)))) by A72, A79;

now :: thesis:

given v being object such that A89: v in (G . x) /\ (G . y) ; :: thesis:
v in G . y by A89, XBOOLE_0:def 4;
then v in great_eq_dom (f,n) by A86, XBOOLE_0:def 4;
then A90: n <= f . v by MESFUNC1:def 14;
v in G . x by A89, XBOOLE_0:def 4;
then v in less_dom (f,(x1 / (2 |^ n))) by A88, XBOOLE_0:def 4;
then f . v < x1 / (2 |^ n) by MESFUNC1:def 11;
then n < x1 / (2 |^ n) by A90, XXREAL_0:2;
hence contradiction by A87, PREPOWER:6, XREAL_1:79; :: thesis:

end;

then (G . x) /\ (G . y) = {} by XBOOLE_0:def 1;
hence G . x misses G . y ; :: thesis:

end;

assume y1 <> ((2 |^ n) * n) + 1 ; :: thesis:
then y1 < (N * n) + 1 by A82, XXREAL_0:1;
then A91: y1 <= N * n by NAT_1:13;
then x1 <= (2 |^ n) * n by A84, XXREAL_0:2;
then A92: G . x = (A /\ (great_eq_dom (f,((x1 - 1) / (2 |^ n))))) /\ (less_dom (f,(x1 / (2 |^ n)))) by A72, A79;
A93: G . y = (A /\ (great_eq_dom (f,((y1 - 1) / (2 |^ n))))) /\ (less_dom (f,(y1 / (2 |^ n)))) by A72, A81, A91;

now :: thesis:

given v being object such that A94: v in (G . x) /\ (G . y) ; :: thesis:
v in G . y by A94, XBOOLE_0:def 4;
then v in A /\ (great_eq_dom (f,((y1 - 1) / (2 |^ n)))) by A93, XBOOLE_0:def 4;
then v in great_eq_dom (f,((y1 - 1) / (2 |^ n))) by XBOOLE_0:def 4;
then A95: (y1 - 1) / (2 |^ n) <= f . v by MESFUNC1:def 14;
v in G . x by A94, XBOOLE_0:def 4;
then v in less_dom (f,(x1 / (2 |^ n))) by A92, XBOOLE_0:def 4;
then f . v < x1 / (2 |^ n) by MESFUNC1:def 11;
then (y1 - 1) / (2 |^ n) < x1 / (2 |^ n) by A95, XXREAL_0:2;
then y1 - 1 < x1 by XREAL_1:72;
then y1 < x1 + 1 by XREAL_1:19;
hence contradiction by A84, NAT_1:13; :: thesis:

end;

then (G . x) /\ (G . y) = {} by XBOOLE_0:def 1;
hence G . x misses G . y ; :: thesis:

end;

case A96: y1 < x1 ; :: thesis:

hereby :: thesis:

assume x1 <> ((2 |^ n) * n) + 1 ; :: thesis:
then x1 < (N * n) + 1 by A83, XXREAL_0:1;
then A97: x1 <= N * n by NAT_1:13;
then y1 <= (2 |^ n) * n by A96, XXREAL_0:2;
then A98: G . y = (A /\ (great_eq_dom (f,((y1 - 1) / (2 |^ n))))) /\ (less_dom (f,(y1 / (2 |^ n)))) by A72, A81;
A99: G . x = (A /\ (great_eq_dom (f,((x1 - 1) / (2 |^ n))))) /\ (less_dom (f,(x1 / (2 |^ n)))) by A72, A79, A97;

now :: thesis:

given v being object such that A100: v in (G . x) /\ (G . y) ; :: thesis:
v in G . x by A100, XBOOLE_0:def 4;
then v in A /\ (great_eq_dom (f,((x1 - 1) / (2 |^ n)))) by A99, XBOOLE_0:def 4;
then v in great_eq_dom (f,((x1 - 1) / (2 |^ n))) by XBOOLE_0:def 4;
then A101: (x1 - 1) / (2 |^ n) <= f . v by MESFUNC1:def 14;
v in G . y by A100, XBOOLE_0:def 4;
then v in less_dom (f,(y1 / (2 |^ n))) by A98, XBOOLE_0:def 4;
then f . v < y1 / (2 |^ n) by MESFUNC1:def 11;
then (x1 - 1) / (2 |^ n) < y1 / (2 |^ n) by A101, XXREAL_0:2;
then x1 - 1 < y1 by XREAL_1:72;
then x1 < y1 + 1 by XREAL_1:19;
hence contradiction by A96, NAT_1:13; :: thesis:

end;

then (G . x) /\ (G . y) = {} by XBOOLE_0:def 1;
hence G . x misses G . y ; :: thesis:

end;

assume A102: x1 = ((2 |^ n) * n) + 1 ; :: thesis:
then A103: G . x = A /\ (great_eq_dom (f,n)) by A71, A77;
A104: y1 <= N * n by A96, A102, NAT_1:13;
then A105: G . y = (A /\ (great_eq_dom (f,((y1 - 1) / (2 |^ n))))) /\ (less_dom (f,(y1 / (2 |^ n)))) by A72, A81;

now :: thesis:

given v being object such that A106: v in (G . x) /\ (G . y) ; :: thesis:
v in G . y by A106, XBOOLE_0:def 4;
then v in less_dom (f,(y1 / (2 |^ n))) by A105, XBOOLE_0:def 4;
then A107: f . v < y1 / (2 |^ n) by MESFUNC1:def 11;
v in G . x by A106, XBOOLE_0:def 4;
then v in great_eq_dom (f,n) by A103, XBOOLE_0:def 4;
then n <= f . v by MESFUNC1:def 14;
then n < y1 / (2 |^ n) by A107, XXREAL_0:2;
hence contradiction by A104, PREPOWER:6, XREAL_1:79; :: thesis:

end;

then (G . x) /\ (G . y) = {} by XBOOLE_0:def 1;
hence G . x misses G . y ; :: thesis:

end;

end;

end;

hence G . x misses G . y ; :: thesis:

end;

end;

end;

then reconsider G = G as Finite_Sep_Sequence of S by PROB_2:def 2;
A108: for k being Nat
for x, y being Element of X st k in dom G & x in G . k & y in G . k holds
(F . n) . x = (F . n) . y

proof

let k be Nat; :: thesis:
let x, y be Element of X; :: thesis:
assume that
A109: k in dom G and
A110: x in G . k and
A111: y in G . k ; :: thesis:
A112: 1 <= k by A71, A109, FINSEQ_1:1;
A113: k <= (N * n) + 1 by A71, A109, FINSEQ_1:1;

now :: thesis:

per cases ;

suppose k = (N * n) + 1 ; :: thesis:

then A114: G . k = A /\ (great_eq_dom (f,n)) by A71, A109;
then x in great_eq_dom (f,n) by A110, XBOOLE_0:def 4;
then A115: n <= f . x by MESFUNC1:def 14;
y in great_eq_dom (f,n) by A111, A114, XBOOLE_0:def 4;
then A116: n <= f . y by MESFUNC1:def 14;
x in A by A110, A114, XBOOLE_0:def 4;
then A117: (F . nn) . x = nn by A26, A24, A115;
y in A by A111, A114, XBOOLE_0:def 4;
hence (F . n) . x = (F . n) . y by A26, A24, A117, A116; :: thesis:

end;

suppose k <> (N * n) + 1 ; :: thesis:

then k < (N * n) + 1 by A113, XXREAL_0:1;
then A118: k <= N * n by NAT_1:13;
then A119: G . k = (A /\ (great_eq_dom (f,((k - 1) / (2 |^ n))))) /\ (less_dom (f,(k / (2 |^ n)))) by A71, A109;
then x in less_dom (f,(k / (2 |^ n))) by A110, XBOOLE_0:def 4;
then A120: f . x < k / (2 |^ n) by MESFUNC1:def 11;
A121: x in A /\ (great_eq_dom (f,((k - 1) / (2 |^ n)))) by A110, A119, XBOOLE_0:def 4;
then x in great_eq_dom (f,((k - 1) / (2 |^ n))) by XBOOLE_0:def 4;
then A122: (k - 1) / (2 |^ n) <= f . x by MESFUNC1:def 14;
x in A by A121, XBOOLE_0:def 4;
then A123: (F . n) . x = (k - 1) / (2 |^ n) by A26, A24, A112, A118, A120, A122;
y in less_dom (f,(k / (2 |^ n))) by A111, A119, XBOOLE_0:def 4;
then A124: f . y < k / (2 |^ n) by MESFUNC1:def 11;
A125: y in A /\ (great_eq_dom (f,((k - 1) / (2 |^ n)))) by A111, A119, XBOOLE_0:def 4;
then y in great_eq_dom (f,((k - 1) / (2 |^ n))) by XBOOLE_0:def 4;
then A126: (k - 1) / (2 |^ n) <= f . y by MESFUNC1:def 14;
y in A by A125, XBOOLE_0:def 4;
hence (F . n) . x = (F . n) . y by A26, A24, A112, A118, A124, A126, A123; :: thesis:

end;

end;

end;

hence (F . n) . x = (F . n) . y ; :: thesis:

end;

for v being object st v in dom f holds
v in union (rng G)

proof

let v be object ; :: thesis:
reconsider vv = v as set by TARSKI:1;
assume A127: v in dom f ; :: thesis:
ex B being set st
( v in B & B in rng G )

proof

per cases ;

suppose A128: f . v < n ; :: thesis:

0 <= f . v by A2, SUPINF_2:51;
then consider k being Nat such that
A129: 1 <= k and
A130: k <= (2 |^ n) * n and
A131: (k - 1) / (2 |^ n) <= f . vv and
A132: f . vv < k / (2 |^ n) by A128, Th4;
v in great_eq_dom (f,((k - 1) / (2 |^ n))) by A127, A131, MESFUNC1:def 14;
then A133: v in A /\ (great_eq_dom (f,((k - 1) / (2 |^ n)))) by A26, A127, XBOOLE_0:def 4;
v in less_dom (f,(k / (2 |^ n))) by A127, A132, MESFUNC1:def 11;
then A134: v in (A /\ (great_eq_dom (f,((k - 1) / (2 |^ n))))) /\ (less_dom (f,(k / (2 |^ n)))) by A133, XBOOLE_0:def 4;
take G . k ; :: thesis:
N * n <= (N * n) + 1 by NAT_1:11;
then k <= (N * n) + 1 by A130, XXREAL_0:2;
then k in Seg ((N * n) + 1) by A129;
hence ( v in G . k & G . k in rng G ) by A71, A130, A134, FUNCT_1:3; :: thesis:

end;

suppose A135: n <= f . v ; :: thesis:

set k = (N * n) + 1;
take G . ((N * n) + 1) ; :: thesis:
1 <= (N * n) + 1 by NAT_1:11;
then A136: (N * n) + 1 in Seg ((N * n) + 1) ;
v in great_eq_dom (f,n) by A127, A135, MESFUNC1:def 14;
then v in A /\ (great_eq_dom (f,n)) by A26, A127, XBOOLE_0:def 4;
hence ( v in G . ((N * n) + 1) & G . ((N * n) + 1) in rng G ) by A71, A136, FUNCT_1:3; :: thesis:

end;

end;

end;

hence v in union (rng G) by TARSKI:def 4; :: thesis:

end;

then A137: dom f c= union (rng G) ;
for v being object st v in union (rng G) holds
v in dom f

proof

let v be object ; :: thesis:
assume v in union (rng G) ; :: thesis:
then consider B being set such that
A138: v in B and
A139: B in rng G by TARSKI:def 4;
consider m being object such that
A140: m in dom G and
A141: B = G . m by A139, FUNCT_1:def 3;
reconsider m = m as Element of NAT by A140;
reconsider mm = m as Nat ;
A142: m <= (N * n) + 1 by A71, A140, FINSEQ_1:1;

now :: thesis:

per cases ;

suppose m = (N * n) + 1 ; :: thesis:

then B = A /\ (great_eq_dom (f,n)) by A71, A140, A141;
hence v in A by A138, XBOOLE_0:def 4; :: thesis:

end;

suppose m <> (N * n) + 1 ; :: thesis:

then m < (N * n) + 1 by A142, XXREAL_0:1;
then m <= N * n by NAT_1:13;
then B = (A /\ (great_eq_dom (f,((mm - 1) / (2 |^ n))))) /\ (less_dom (f,(mm / (2 |^ n)))) by A71, A140, A141;
then v in A /\ (great_eq_dom (f,((m - 1) / (2 |^ n)))) by A138, XBOOLE_0:def 4;
hence v in A by XBOOLE_0:def 4; :: thesis:

end;

end;

end;

hence v in dom f by A26; :: thesis:

end;

then union (rng G) c= dom f ;
then union (rng G) = dom f by A137;
then dom (F . n) = union (rng G) by A25;
hence F . n is_simple_func_in S by A67, A108, MESFUNC2:def 4; :: thesis:

end;

A143: now :: thesis:

let x be Element of X; :: thesis:
assume A144: x in dom f ; :: thesis:

per cases = +infty or |.(f . x).| <> +infty ) ;

suppose A145: |.(f . x).| = +infty ; :: thesis:

now :: thesis:

assume - (f . x) = +infty ; :: thesis:
then f . x < 0 ;
hence contradiction by A2, SUPINF_2:51; :: thesis:

end;

then A146: f . x = +infty by A145, EXTREAL1:13;
for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= (F # x) . m

proof

let g be Real; :: thesis:
assume 0 < g ; :: thesis:
then reconsider n = [/g\] as Nat by INT_1:53;
A147: g <= n by INT_1:def 7;
for m being Nat st n <= m holds
g <= (F # x) . m

proof

let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then A148: g <= m by A147, XXREAL_0:2;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
m <= f . x by A146, XXREAL_0:4;
then (F . m) . x = m by A24, A144;
hence g <= (F # x) . m by A148, Def13; :: thesis:

end;

hence ex n being Nat st
for m being Nat st n <= m holds
g <= (F # x) . m ; :: thesis:

end;

then A149: F # x is convergent_to_+infty ;
then F # x is convergent ;
hence ( F # x is convergent & lim (F # x) = f . x ) by A146, A149, Def12; :: thesis:

end;

suppose |.(f . x).| <> +infty ; :: thesis:

then reconsider g = f . x as Element of REAL by EXTREAL1:30, XXREAL_0:14;
A150: for p being Real st 0 < p holds
ex k being Nat st
for j being Nat st j >= k holds
|.(((F # x) . j) - (f . x)).| < p

proof

set N2 = [/g\] + 1;
let p be Real; :: thesis:
A151: g <= [/g\] by INT_1:def 7;
[/g\] < [/g\] + 1 by XREAL_1:29;
then A152: g < [/g\] + 1 by A151, XXREAL_0:2;
0 <= g by A2, SUPINF_2:51;
then reconsider N2 = [/g\] + 1 as Element of NAT by A151, INT_1:3;
A153: for N being Nat st N >= N2 holds
|.(((F # x) . N) - (f . x)).| < 1 / (2 |^ N)

proof

let N be Nat; :: thesis:
assume A154: N >= N2 ; :: thesis:
reconsider NN = N as Element of NAT by ORDINAL1:def 12;
A155: 0 <= f . x by A2, SUPINF_2:51;
f . x < N by A152, A154, XXREAL_0:2;
then consider m being Nat such that
A156: 1 <= m and
A157: m <= (2 |^ N) * N and
A158: (m - 1) / (2 |^ N) <= f . x and
A159: f . x < m / (2 |^ N) by A155, Th4;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
A160: (F # x) . N = (F . NN) . x by Def13
.= (m - 1) / (2 |^ NN) by A24, A144, A156, A157, A158, A159 ;
then A161: (F # x) . N in REAL by XREAL_0:def 1;
(m / (2 |^ N)) - ((m - 1) / (2 |^ N)) = (m / (2 |^ N)) - ((m - 1) / (2 |^ N))
.= (m / (2 |^ N)) + (- ((m - 1) / (2 |^ N)))
.= (m / (2 |^ N)) + ((- (m - 1)) / (2 |^ N))
.= (m + (- (m - 1))) / (2 |^ N) ;
then A162: (f . x) - ((F # x) . N) < 1 / (2 |^ N) by A159, A160, XXREAL_3:43, A161;
- (((F # x) . N) - (f . x)) = (f . x) - ((F # x) . N) by XXREAL_3:26;
then A163: |.(((F # x) . N) - (f . x)).| = |.((f . x) - ((F # x) . N)).| by EXTREAL1:29;
2 |^ N > 0 by PREPOWER:6;
then A164: - (1 / (2 |^ N)) < 0 ;
0 <= (f . x) - ((F # x) . N) by A158, A160, XXREAL_3:40;
hence |.(((F # x) . N) - (f . x)).| < 1 / (2 |^ N) by A163, A162, A164, EXTREAL1:22; :: thesis:

end;

assume 0 < p ; :: thesis:
then consider N1 being Nat such that
A165: 1 / (2 |^ N1) <= p by PREPOWER:92;
reconsider k = max (N2,N1) as Element of NAT by ORDINAL1:def 12;
A166: for k being Nat st k >= N1 holds
1 / (2 |^ k) <= p

proof

let k be Nat; :: thesis:
assume k >= N1 ; :: thesis:
then consider i being Nat such that
A167: k = N1 + i by NAT_1:10;
(2 |^ N1) * (2 |^ i) >= 2 |^ N1 by PREPOWER:11, XREAL_1:151;
then A168: 2 |^ k >= 2 |^ N1 by A167, NEWTON:8;
2 |^ N1 > 0 by PREPOWER:11;
then (2 |^ k) " <= (2 |^ N1) " by A168, XREAL_1:85;
then 1 / (2 |^ k) <= (2 |^ N1) " ;
then 1 / (2 |^ k) <= 1 / (2 |^ N1) ;
hence 1 / (2 |^ k) <= p by A165, XXREAL_0:2; :: thesis:

end;

now :: thesis:

let j be Nat; :: thesis:
assume A169: j >= k ; :: thesis:
k >= N2 by XXREAL_0:25;
then j >= N2 by A169, XXREAL_0:2;
then A170: |.(((F # x) . j) - (f . x)).| < 1 / (2 |^ j) by A153;
k >= N1 by XXREAL_0:25;
then j >= N1 by A169, XXREAL_0:2;
then 1 / (2 |^ j) <= p by A166;
hence |.(((F # x) . j) - (f . x)).| < p by A170, XXREAL_0:2; :: thesis:

end;

hence ex k being Nat st
for j being Nat st j >= k holds
|.(((F # x) . j) - (f . x)).| < p ; :: thesis:

end;

A171: f . x = g ;
then A172: F # x is convergent_to_finite_number by A150;
then F # x is convergent ;
hence ( F # x is convergent & lim (F # x) = f . x ) by A171, A150, A172, Def12; :: thesis:

end;

end;

end;

for n being Nat holds F . n is nonnegative

proof

let n be Nat; :: thesis:
reconsider nn = n as Element of NAT by ORDINAL1:def 12;

now :: thesis:

let x be object ; :: thesis:
assume x in dom (F . n) ; :: thesis:
then A173: x in dom f by A25;

per cases ;

suppose n <= f . x ; :: thesis:

hence 0 <= (F . nn) . x by A24, A173; :: thesis:

end;

suppose A174: f . x < n ; :: thesis:

0 <= f . x by A2, SUPINF_2:51;
then consider k being Nat such that
A175: 1 <= k and
A176: k <= (2 |^ n) * n and
A177: (k - 1) / (2 |^ n) <= f . x and
A178: f . x < k / (2 |^ n) by A174, Th4;
thus 0 <= (F . nn) . x by A24, A173, A175, A176, A177, A178; :: thesis:

end;

end;

end;

hence F . n is nonnegative by SUPINF_2:52; :: thesis:

end;

hence ex F being Functional_Sequence of X,ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) ) by A25, A51, A28, A143; :: thesis: