let X be non empty set ; :: thesis: for S being SigmaField of X

for f being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

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

let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

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

let f be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative implies 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 ) ) ) )

assume that

A1: ex A being Element of S st

( A = dom f & f is A -measurable ) and

A2: f is nonnegative ; :: thesis: 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 ) ) )

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

A22: for n being Element of NAT holds S_{1}[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;

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

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

for f being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

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

let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative holds

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

let f be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st

( A = dom f & f is A -measurable ) & f is nonnegative implies 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 ) ) ) )

assume that

A1: ex A being Element of S st

( A = dom f & f is A -measurable ) and

A2: f is nonnegative ; :: thesis: 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 ) ) )

defpred S

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

proof

consider F being sequence of (PFuncs (X,ExtREAL)) such that
let n be Element of NAT ; :: thesis: ex y being Element of PFuncs (X,ExtREAL) st S_{1}[n,y]

reconsider nn = n as Nat ;

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

A14: ( dom fn = dom f & ( for x being object st x in dom f holds

S_{2}[x,fn . x] ) )
from CLASSES1:sch 1(A4);

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: S_{1}[n,y]

thus S_{1}[n,y]
by A14; :: thesis: verum

end;reconsider nn = n as Nat ;

defpred S

$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

proof

consider fn being Function such that
let x be object ; :: thesis: ( x in dom f implies ex y being object st S_{2}[x,y] )

assume x in dom f ; :: thesis: ex y being object st S_{2}[x,y]

end;assume x in dom f ; :: thesis: ex y being object st S

per cases
( f . x < n or n <= f . x )
;

end;

suppose A5:
f . x < n
; :: thesis: ex y being object st S_{2}[x,y]

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: S_{2}[x,y]

_{2}[x,y]
by A5; :: thesis: verum

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

now :: thesis: for k1 being Nat st 1 <= k1 & k1 <= (2 |^ n) * n & (k1 - 1) / (2 |^ n) <= f . x & f . x < k1 / (2 |^ n) holds

y = (k1 - 1) / (2 |^ n)

hence
Sy = (k1 - 1) / (2 |^ n)

let k1 be Nat; :: thesis: ( 1 <= k1 & k1 <= (2 |^ n) * n & (k1 - 1) / (2 |^ n) <= f . x & f . x < k1 / (2 |^ n) implies y = (k1 - 1) / (2 |^ n) )

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: y = (k1 - 1) / (2 |^ n)

end;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: y = (k1 - 1) / (2 |^ n)

A10: now :: thesis: not k1 < k

assume
k1 < k
; :: thesis: contradiction

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

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

now :: thesis: not k < k1

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

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

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

suppose A11:
n <= f . x
; :: thesis: ex y being object st S_{2}[x,y]

reconsider y = nn as Real ;

take y ; :: thesis: S_{2}[x,y]

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: ( n <= f . x implies y = n )

end;take y ; :: thesis: S

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: ( n <= f . x implies y = n )

proof

thus
( n <= f . x implies y = n )
; :: thesis: verum
let k be Nat; :: thesis: ( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= f . x & f . x < k / (2 |^ n) implies y = (k - 1) / (2 |^ n) )

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: y = (k - 1) / (2 |^ n)

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

end;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: y = (k - 1) / (2 |^ n)

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

A14: ( dom fn = dom f & ( for x being object st x in dom f holds

S

now :: thesis: for w being object st w in rng fn holds

w in ExtREAL

then
rng fn c= ExtREAL
;w in ExtREAL

let w be object ; :: thesis: ( w in rng fn implies b_{1} in ExtREAL )

assume w in rng fn ; :: thesis: b_{1} in ExtREAL

then consider v being object such that

A15: v in dom fn and

A16: w = fn . v by FUNCT_1:def 3;

end;assume w in rng fn ; :: thesis: b

then consider v being object such that

A15: v in dom fn and

A16: w = fn . v by FUNCT_1:def 3;

per cases
( n <= f . v or f . v < n )
;

end;

suppose A17:
f . v < n
; :: thesis: b_{1} in ExtREAL

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

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

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

thus S

A22: for n being Element of NAT holds S

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: for n being Nat holds dom (F . n) = dom f

reconsider F = F as Functional_Sequence of X,ExtREAL ;let n be Nat; :: thesis: dom (F . n) = dom f

n in NAT by ORDINAL1:def 12;

hence dom (F . n) = dom f by A23; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence dom (F . n) = dom f by A23; :: thesis: verum

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

A51:
for n being Nat holds F . n is_simple_func_in S
let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x )

assume A29: n <= m ; :: thesis: for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x

reconsider nn = n, mm = m as Element of NAT by ORDINAL1:def 12;

let x be Element of X; :: thesis: ( x in dom f implies (F . n) . x <= (F . m) . x )

assume A30: x in dom f ; :: thesis: (F . n) . x <= (F . m) . x

end;(F . n) . x <= (F . m) . x )

assume A29: n <= m ; :: thesis: for x being Element of X st x in dom f holds

(F . n) . x <= (F . m) . x

reconsider nn = n, mm = m as Element of NAT by ORDINAL1:def 12;

let x be Element of X; :: thesis: ( x in dom f implies (F . n) . x <= (F . m) . x )

assume A30: x in dom f ; :: thesis: (F . n) . x <= (F . m) . x

per cases
( m <= f . x or f . x < m )
;

end;

suppose A31:
m <= f . x
; :: thesis: (F . n) . x <= (F . m) . x

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

end;(F . mm) . x = m by A24, A30, A31;

hence (F . n) . x <= (F . m) . x by A24, A29, A30, A32; :: thesis: verum

suppose A33:
f . x < m
; :: thesis: (F . n) . x <= (F . m) . x

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;

end;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
( n <= f . x or f . x < n )
;

end;

suppose A40:
n <= f . x
; :: thesis: (F . n) . x <= (F . m) . x

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

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

suppose A43:
f . x < n
; :: thesis: (F . n) . x <= (F . m) . x

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

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

proof

let n be Nat; :: thesis: F . n is_simple_func_in S

reconsider nn = n as Element of NAT by ORDINAL1:def 12;

reconsider N = 2 |^ nn as Element of NAT ;

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

A71: ( dom G = Seg ((N * n) + 1) & ( for k being Nat st k in Seg ((N * n) + 1) holds

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

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

v in union (rng G)

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

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

end;reconsider nn = n as Element of NAT by ORDINAL1:def 12;

reconsider N = 2 |^ nn as Element of NAT ;

defpred S

now :: thesis: for x being Element of X st x in dom (F . n) holds

|.((F . n) . x).| < +infty

then A67:
F . n is real-valued
by MESFUNC2:def 1;|.((F . n) . x).| < +infty

let x be Element of X; :: thesis: ( x in dom (F . n) implies |.((F . n) . b_{1}).| < +infty )

assume x in dom (F . n) ; :: thesis: |.((F . n) . b_{1}).| < +infty

then A52: x in dom f by A25;

end;assume x in dom (F . n) ; :: thesis: |.((F . n) . b

then A52: x in dom f by A25;

per cases
( n <= f . x or f . x < n )
;

end;

suppose A53:
n <= f . x
; :: thesis: |.((F . n) . b_{1}).| < +infty

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

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

suppose A55:
f . x < n
; :: thesis: |.((F . n) . b_{1}).| < +infty

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

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

A68: now :: thesis: for k being Nat st k in Seg ((N * n) + 1) holds

ex B being Element of S st S_{2}[k,B]

consider G being FinSequence of S such that ex B being Element of S st S

let k be Nat; :: thesis: ( k in Seg ((N * n) + 1) implies ex B being Element of S st S_{2}[B,b_{2}] )

assume k in Seg ((N * n) + 1) ; :: thesis: ex B being Element of S st S_{2}[B,b_{2}]

reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

end;assume k in Seg ((N * n) + 1) ; :: thesis: ex B being Element of S st S

reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

per cases
( k <> (N * n) + 1 or k = (N * n) + 1 )
;

end;

suppose A69:
k <> (N * n) + 1
; :: thesis: ex B being Element of S st S_{2}[B,b_{2}]

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: S_{2}[k,B]

thus S_{2}[k,B]
by A69; :: thesis: verum

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

thus S

suppose A70:
k = (N * n) + 1
; :: thesis: ex B being Element of S st S_{2}[B,b_{2}]

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: S_{2}[k,B]

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

end;reconsider B = A /\ (great_eq_dom (f,n)) as Element of S by A26, A27, MESFUNC1:27;

take B = B; :: thesis: S

thus S

A71: ( dom G = Seg ((N * n) + 1) & ( for k being Nat st k in Seg ((N * n) + 1) holds

S

A72: now :: thesis: for k being Nat st 1 <= k & k <= (2 |^ n) * n holds

G . k = (A /\ (great_eq_dom (f,((k - 1) / (2 |^ n))))) /\ (less_dom (f,(k / (2 |^ n))))

A75:
len G = ((2 |^ n) * n) + 1
by A71, FINSEQ_1:def 3;G . k = (A /\ (great_eq_dom (f,((k - 1) / (2 |^ n))))) /\ (less_dom (f,(k / (2 |^ n))))

let k be Nat; :: thesis: ( 1 <= k & k <= (2 |^ n) * n implies G . k = (A /\ (great_eq_dom (f,((k - 1) / (2 |^ n))))) /\ (less_dom (f,(k / (2 |^ n)))) )

assume that

A73: 1 <= k and

A74: k <= (2 |^ n) * n ; :: thesis: G . k = (A /\ (great_eq_dom (f,((k - 1) / (2 |^ n))))) /\ (less_dom (f,(k / (2 |^ n))))

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

end;assume that

A73: 1 <= k and

A74: k <= (2 |^ n) * n ; :: thesis: G . k = (A /\ (great_eq_dom (f,((k - 1) / (2 |^ n))))) /\ (less_dom (f,(k / (2 |^ n))))

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

now :: thesis: for x, y being object st x <> y holds

G . x misses G . y

then reconsider G = G as Finite_Sep_Sequence of S by PROB_2:def 2;G . x misses G . y

let x, y be object ; :: thesis: ( x <> y implies G . b_{1} misses G . b_{2} )

assume A76: x <> y ; :: thesis: G . b_{1} misses G . b_{2}

end;assume A76: x <> y ; :: thesis: G . b

per cases
( not x in dom G or not y in dom G or ( x in dom G & y in dom G ) )
;

end;

suppose A77:
( x in dom G & y in dom G )
; :: thesis: G . b_{1} misses G . b_{2}

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;

end;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: ( ( x1 < y1 & ( y1 = ((2 |^ n) * n) + 1 implies G . x misses G . y ) & ( y1 <> ((2 |^ n) * n) + 1 implies G . x misses G . y ) ) or ( y1 < x1 & ( x1 <> ((2 |^ n) * n) + 1 implies G . x misses G . y ) & ( x1 = ((2 |^ n) * n) + 1 implies G . x misses G . y ) ) )end;

hence
G . x misses G . y
; :: thesis: verumper cases
( x1 < y1 or y1 < x1 )
by A76, XXREAL_0:1;

end;

case A84:
x1 < y1
; :: thesis: ( ( y1 = ((2 |^ n) * n) + 1 implies G . x misses G . y ) & ( y1 <> ((2 |^ n) * n) + 1 implies G . x misses G . y ) )

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;

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

end;

hereby :: thesis: ( y1 <> ((2 |^ n) * n) + 1 implies G . x misses G . y )

assume
y1 <> ((2 |^ n) * n) + 1
; :: thesis: G . x misses G . yassume A85:
y1 = ((2 |^ n) * n) + 1
; :: thesis: G . x misses G . y

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;

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

end;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: for v being object holds not v in (G . x) /\ (G . y)

then
(G . x) /\ (G . y) = {}
by XBOOLE_0:def 1;given v being object such that A89:
v in (G . x) /\ (G . y)
; :: thesis: contradiction

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

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

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

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: for v being object holds not v in (G . x) /\ (G . y)

then
(G . x) /\ (G . y) = {}
by XBOOLE_0:def 1;given v being object such that A94:
v in (G . x) /\ (G . y)
; :: thesis: contradiction

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

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

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

case A96:
y1 < x1
; :: thesis: ( ( x1 <> ((2 |^ n) * n) + 1 implies G . x misses G . y ) & ( x1 = ((2 |^ n) * n) + 1 implies G . x misses G . y ) )

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;

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

end;

hereby :: thesis: ( x1 = ((2 |^ n) * n) + 1 implies G . x misses G . y )

assume A102:
x1 = ((2 |^ n) * n) + 1
; :: thesis: G . x misses G . yassume
x1 <> ((2 |^ n) * n) + 1
; :: thesis: G . x misses G . y

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;

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

end;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: for v being object holds not v in (G . x) /\ (G . y)

then
(G . x) /\ (G . y) = {}
by XBOOLE_0:def 1;given v being object such that A100:
v in (G . x) /\ (G . y)
; :: thesis: contradiction

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

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

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

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: for v being object holds not v in (G . x) /\ (G . y)

then
(G . x) /\ (G . y) = {}
by XBOOLE_0:def 1;given v being object such that A106:
v in (G . x) /\ (G . y)
; :: thesis: contradiction

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

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

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

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

for v being object st v in dom f holds
let k be Nat; :: thesis: 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

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

assume that

A109: k in dom G and

A110: x in G . k and

A111: y in G . k ; :: thesis: (F . n) . x = (F . n) . y

A112: 1 <= k by A71, A109, FINSEQ_1:1;

A113: k <= (N * n) + 1 by A71, A109, FINSEQ_1:1;

end;(F . n) . x = (F . n) . y

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

assume that

A109: k in dom G and

A110: x in G . k and

A111: y in G . k ; :: thesis: (F . n) . x = (F . n) . y

A112: 1 <= k by A71, A109, FINSEQ_1:1;

A113: k <= (N * n) + 1 by A71, A109, FINSEQ_1:1;

now :: thesis: (F . n) . x = (F . n) . yend;

hence
(F . n) . x = (F . n) . y
; :: thesis: verumper cases
( k = (N * n) + 1 or k <> (N * n) + 1 )
;

end;

suppose
k = (N * n) + 1
; :: thesis: (F . n) . x = (F . n) . y

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

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

suppose
k <> (N * n) + 1
; :: thesis: (F . n) . x = (F . n) . y

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

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

v in union (rng G)

proof

then A137:
dom f c= union (rng G)
;
let v be object ; :: thesis: ( v in dom f implies v in union (rng G) )

reconsider vv = v as set by TARSKI:1;

assume A127: v in dom f ; :: thesis: v in union (rng G)

ex B being set st

( v in B & B in rng G )

end;reconsider vv = v as set by TARSKI:1;

assume A127: v in dom f ; :: thesis: v in union (rng G)

ex B being set st

( v in B & B in rng G )

proof
end;

hence
v in union (rng G)
by TARSKI:def 4; :: thesis: verumper cases
( f . v < n or n <= f . v )
;

end;

suppose A128:
f . v < n
; :: thesis: ex B being set st

( v in B & B in rng G )

( v in B & B in rng G )

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: ( v in G . k & G . k in rng G )

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

end;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: ( v in G . k & G . k in rng G )

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

suppose A135:
n <= f . v
; :: thesis: ex B being set st

( v in B & B in rng G )

( v in B & B in rng G )

set k = (N * n) + 1;

take G . ((N * n) + 1) ; :: thesis: ( v in G . ((N * n) + 1) & G . ((N * n) + 1) in rng G )

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

end;take G . ((N * n) + 1) ; :: thesis: ( v in G . ((N * n) + 1) & G . ((N * n) + 1) in rng G )

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

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

v in dom f

proof

then
union (rng G) c= dom f
;
let v be object ; :: thesis: ( v in union (rng G) implies v in dom f )

assume v in union (rng G) ; :: thesis: v in dom f

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;

end;assume v in union (rng G) ; :: thesis: v in dom f

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: v in Aend;

hence
v in dom f
by A26; :: thesis: verumper cases
( m = (N * n) + 1 or m <> (N * n) + 1 )
;

end;

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

then
B = A /\ (great_eq_dom (f,n))
by A71, A140, A141;

hence v in A by A138, XBOOLE_0:def 4; :: thesis: verum

end;hence v in A by A138, XBOOLE_0:def 4; :: thesis: verum

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

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

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

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

A143: now :: thesis: for x being Element of X st x in dom f holds

( F # x is convergent & lim (F # x) = f . x )

for n being Nat holds F . n is nonnegative
( F # x is convergent & lim (F # x) = f . x )

let x be Element of X; :: thesis: ( x in dom f implies ( F # b_{1} is convergent & lim (F # b_{1}) = f . b_{1} ) )

assume A144: x in dom f ; :: thesis: ( F # b_{1} is convergent & lim (F # b_{1}) = f . b_{1} )

end;assume A144: x in dom f ; :: thesis: ( F # b

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

end;

suppose A145:
|.(f . x).| = +infty
; :: thesis: ( F # b_{1} is convergent & lim (F # b_{1}) = f . b_{1} )

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

then F # x is convergent ;

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

end;

now :: thesis: not - (f . x) = +infty

then A146:
f . x = +infty
by A145, EXTREAL1:13;assume
- (f . x) = +infty
; :: thesis: contradiction

then f . x < 0 ;

hence contradiction by A2, SUPINF_2:51; :: thesis: verum

end;then f . x < 0 ;

hence contradiction by A2, SUPINF_2:51; :: thesis: verum

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

then A149:
F # x is convergent_to_+infty
;
let g be Real; :: thesis: ( 0 < g implies ex n being Nat st

for m being Nat st n <= m holds

g <= (F # x) . m )

assume 0 < g ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

g <= (F # x) . m

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

for m being Nat st n <= m holds

g <= (F # x) . m ; :: thesis: verum

end;for m being Nat st n <= m holds

g <= (F # x) . m )

assume 0 < g ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

g <= (F # x) . m

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

hence
ex n being Nat st
let m be Nat; :: thesis: ( n <= m implies g <= (F # x) . m )

assume n <= m ; :: thesis: g <= (F # x) . m

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

end;assume n <= m ; :: thesis: g <= (F # x) . m

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

for m being Nat st n <= m holds

g <= (F # x) . m ; :: thesis: verum

then F # x is convergent ;

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

suppose
|.(f . x).| <> +infty
; :: thesis: ( F # b_{1} is convergent & lim (F # b_{1}) = f . b_{1} )

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

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

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

A171:
f . x = g
;
set N2 = [/g\] + 1;

let p be Real; :: thesis: ( 0 < p implies ex k being Nat st

for j being Nat st j >= k holds

|.(((F # x) . j) - (f . x)).| < p )

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)

for j being Nat st j >= k holds

|.(((F # x) . j) - (f . x)).| < p

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

for j being Nat st j >= k holds

|.(((F # x) . j) - (f . x)).| < p ; :: thesis: verum

end;let p be Real; :: thesis: ( 0 < p implies ex k being Nat st

for j being Nat st j >= k holds

|.(((F # x) . j) - (f . x)).| < p )

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

assume
0 < p
; :: thesis: ex k being Nat st
let N be Nat; :: thesis: ( N >= N2 implies |.(((F # x) . N) - (f . x)).| < 1 / (2 |^ N) )

assume A154: N >= N2 ; :: thesis: |.(((F # x) . N) - (f . x)).| < 1 / (2 |^ N)

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

end;assume A154: N >= N2 ; :: thesis: |.(((F # x) . N) - (f . x)).| < 1 / (2 |^ N)

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

for j being Nat st j >= k holds

|.(((F # x) . j) - (f . x)).| < p

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: ( k >= N1 implies 1 / (2 |^ k) <= p )

assume k >= N1 ; :: thesis: 1 / (2 |^ k) <= p

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

end;assume k >= N1 ; :: thesis: 1 / (2 |^ k) <= p

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

now :: thesis: for j being Nat st j >= k holds

|.(((F # x) . j) - (f . x)).| < p

hence
ex k being Nat st |.(((F # x) . j) - (f . x)).| < p

let j be Nat; :: thesis: ( j >= k implies |.(((F # x) . j) - (f . x)).| < p )

assume A169: j >= k ; :: thesis: |.(((F # x) . j) - (f . x)).| < p

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

end;assume A169: j >= k ; :: thesis: |.(((F # x) . j) - (f . x)).| < p

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

for j being Nat st j >= k holds

|.(((F # x) . j) - (f . x)).| < p ; :: thesis: verum

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

proof

hence
ex F being Functional_Sequence of X,ExtREAL st
let n be Nat; :: thesis: F . n is nonnegative

reconsider nn = n as Element of NAT by ORDINAL1:def 12;

end;reconsider nn = n as Element of NAT by ORDINAL1:def 12;

now :: thesis: for x being object st x in dom (F . n) holds

0 <= (F . nn) . x

hence
F . n is nonnegative
by SUPINF_2:52; :: thesis: verum0 <= (F . nn) . x

let x be object ; :: thesis: ( x in dom (F . n) implies 0 <= (F . nn) . b_{1} )

assume x in dom (F . n) ; :: thesis: 0 <= (F . nn) . b_{1}

then A173: x in dom f by A25;

end;assume x in dom (F . n) ; :: thesis: 0 <= (F . nn) . b

then A173: x in dom f by A25;

per cases
( n <= f . x or f . x < n )
;

end;

suppose A174:
f . x < n
; :: thesis: 0 <= (F . nn) . b_{1}

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

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

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