let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st [.a,b.[ = dom f holds
ex F being Functional_Sequence of REAL,REAL st
( ( for n being Nat holds
( dom (F . n) = dom f & ( for x being Real st x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = f . x ) & ( for x being Real st not x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = 0 ) ) ) & lim (R_EAL F) = f )
let a, b be Real; :: thesis: ( [.a,b.[ = dom f implies ex F being Functional_Sequence of REAL,REAL st
( ( for n being Nat holds
( dom (F . n) = dom f & ( for x being Real st x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = f . x ) & ( for x being Real st not x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = 0 ) ) ) & lim (R_EAL F) = f ) )
assume A1: [.a,b.[ = dom f ; :: thesis: ex F being Functional_Sequence of REAL,REAL st
( ( for n being Nat holds
( dom (F . n) = dom f & ( for x being Real st x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = f . x ) & ( for x being Real st not x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = 0 ) ) ) & lim (R_EAL F) = f )
A2: for n being Element of NAT holds [.a,(b - (1 / (n + 1))).] c= dom f
proof
let n be Element of NAT ; :: thesis: [.a,(b - (1 / (n + 1))).] c= dom f
b - (1 / (n + 1)) < b by XREAL_1:44;
hence [.a,(b - (1 / (n + 1))).] c= dom f by A1, XXREAL_1:43; :: thesis: verum
end;
defpred S1[ Element of NAT , object ] means $2 = chi ([.a,(b - (1 / ($1 + 1))).],(dom f));
A3: for n being Element of NAT ex ch being Element of PFuncs (REAL,REAL) st S1[n,ch]
proof
let n be Element of NAT ; :: thesis: ex ch being Element of PFuncs (REAL,REAL) st S1[n,ch]
dom (chi ([.a,(b - (1 / (n + 1))).],(dom f))) = dom f by FUNCT_3:def 3;
then reconsider ch = chi ([.a,(b - (1 / (n + 1))).],(dom f)) as PartFunc of REAL,REAL by RELSET_1:5;
reconsider ch = ch as Element of PFuncs (REAL,REAL) by PARTFUN1:45;
take ch ; :: thesis: S1[n,ch]
thus S1[n,ch] ; :: thesis: verum
end;
consider CH being sequence of (PFuncs (REAL,REAL)) such that
A4: for n being Element of NAT holds S1[n,CH . n] from FUNCT_2:sch 3(A3);
 defpred S2[ Element of NAT , object ] means $2 = f (#) (CH . $1);
A5: for n being Element of NAT ex F being Element of PFuncs (REAL,REAL) st S2[n,F]
proof
let n be Element of NAT ; :: thesis: ex F being Element of PFuncs (REAL,REAL) st S2[n,F]
reconsider F = f (#) (CH . n) as Element of PFuncs (REAL,REAL) by PARTFUN1:45;
take F ; :: thesis: S2[n,F]
thus S2[n,F] ; :: thesis: verum
end;
consider F being sequence of (PFuncs (REAL,REAL)) such that
A6: for n being Element of NAT holds S2[n,F . n] from FUNCT_2:sch 3(A5);
 take F ; :: thesis: ( ( for n being Nat holds
( dom (F . n) = dom f & ( for x being Real st x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = f . x ) & ( for x being Real st not x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = 0 ) ) ) & lim (R_EAL F) = f )
thus A7: for n being Nat holds
( dom (F . n) = dom f & ( for x being Real st x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = f . x ) & ( for x being Real st not x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = 0 ) ) :: thesis: lim (R_EAL F) = f
proof
let n be Nat; :: thesis: ( dom (F . n) = dom f & ( for x being Real st x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = f . x ) & ( for x being Real st not x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = 0 ) )
A8: n is Element of NAT by ORDINAL1:def 12;
then A9: CH . n = chi ([.a,(b - (1 / (n + 1))).],(dom f)) by A4;
then A10: dom (CH . n) = dom f by FUNCT_3:def 3;
A11: F . n = f (#) (CH . n) by A6, A8;
then A12: dom (F . n) = (dom f) /\ (dom (CH . n)) by VALUED_1:def 4;
hence dom (F . n) = dom f by A10; :: thesis: ( ( for x being Real st x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = f . x ) & ( for x being Real st not x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = 0 ) )
thus for x being Real st x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = f . x :: thesis: for x being Real st not x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = 0
proof
let x be Real; :: thesis: ( x in [.a,(b - (1 / (n + 1))).] implies (F . n) . x = f . x )
assume A13: x in [.a,(b - (1 / (n + 1))).] ; :: thesis: (F . n) . x = f . x
A14: [.a,(b - (1 / (n + 1))).] c= dom f by A8, A2;
then (CH . n) . x = 1 by A9, A13, FUNCT_3:def 3;
then (F . n) . x = (f . x) * 1 by A11, A12, A10, A13, A14, VALUED_1:def 4;
hence (F . n) . x = f . x ; :: thesis: verum
end;
thus for x being Real st not x in [.a,(b - (1 / (n + 1))).] holds
(F . n) . x = 0 :: thesis: verum
proof
let x be Real; :: thesis: ( not x in [.a,(b - (1 / (n + 1))).] implies (F . n) . x = 0 )
assume A15: not x in [.a,(b - (1 / (n + 1))).] ; :: thesis: (F . n) . x = 0
per cases ( x in dom f or not x in dom f ) ;
suppose A16: x in dom f ; :: thesis: (F . n) . x = 0
then (CH . n) . x = 0 by A9, A15, FUNCT_3:def 3;
then (F . n) . x = (f . x) * 0 by A11, A12, A10, A16, VALUED_1:def 4;
hence (F . n) . x = 0 ; :: thesis: verum
end;
suppose not x in dom f ; :: thesis: (F . n) . x = 0
hence (F . n) . x = 0 by A12, A10, FUNCT_1:def 2; :: thesis: verum
end;
end;
end;
end;
dom (lim (R_EAL F)) = dom ((R_EAL F) . 0) by MESFUNC8:def 9;
then dom (lim (R_EAL F)) = dom (F . 0) by MESFUN7C:def 1;
then A17: dom (lim (R_EAL F)) = dom f by A7;
then A18: dom (lim (R_EAL F)) = dom (R_EAL f) by MESFUNC5:def 7;
A19: for x being Element of REAL st x in dom (lim (R_EAL F)) holds
(lim (R_EAL F)) . x = (R_EAL f) . x
proof
let x be Element of REAL ; :: thesis: ( x in dom (lim (R_EAL F)) implies (lim (R_EAL F)) . x = (R_EAL f) . x )
assume A20: x in dom (lim (R_EAL F)) ; :: thesis: (lim (R_EAL F)) . x = (R_EAL f) . x
then A21: ( a <= x & x < b ) by A1, A17, XXREAL_1:3;
then A22: 0 < b - x by XREAL_1:50;
A23: (lim (R_EAL F)) . x = lim ((R_EAL F) # x) by A20, MESFUNC8:def 9;
A24: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((((R_EAL F) # x) . m) - (f . x)).| < p
proof
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((((R_EAL F) # x) . m) - (f . x)).| < p )
assume A25: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((((R_EAL F) # x) . m) - (f . x)).| < p
consider n being Nat such that
A26: 1 / (b - x) < n by SEQ_4:3;
n <= n + 1 by NAT_1:13;
then 1 / (b - x) < 1 * (n + 1) by A26, XXREAL_0:2;
then 1 / (n + 1) < 1 * (b - x) by A22, XREAL_1:113;
then x + (1 / (n + 1)) < b by XREAL_1:20;
then A27: x < b - (1 / (n + 1)) by XREAL_1:20;
take n ; :: thesis: for m being Nat st n <= m holds
|.((((R_EAL F) # x) . m) - (f . x)).| < p
hereby :: thesis: verum
let m be Nat; :: thesis: ( n <= m implies |.((((R_EAL F) # x) . m) - (f . x)).| < p )
assume n <= m ; :: thesis: |.((((R_EAL F) # x) . m) - (f . x)).| < p
then n + 1 <= m + 1 by XREAL_1:6;
then 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:118;
then b - (1 / (n + 1)) <= b - (1 / (m + 1)) by XREAL_1:10;
then x < b - (1 / (m + 1)) by A27, XXREAL_0:2;
then x in [.a,(b - (1 / (m + 1))).] by A21, XXREAL_1:1;
then (F . m) . x = f . x by A7;
then ((R_EAL F) . m) . x = f . x by MESFUN7C:def 1;
then ((R_EAL F) # x) . m = f . x by MESFUNC5:def 13;
then (((R_EAL F) # x) . m) - (f . x) = (((R_EAL F) # x) . m) + (- (((R_EAL F) # x) . m)) by XXREAL_3:def 4;
hence |.((((R_EAL F) # x) . m) - (f . x)).| < p by A25, EXTREAL1:16, XXREAL_3:7; :: thesis: verum
end;
end;
then (R_EAL F) # x is convergent_to_finite_number by MESFUNC5:def 8;
then lim ((R_EAL F) # x) = f . x by A24, MESFUNC5:def 12;
hence (lim (R_EAL F)) . x = (R_EAL f) . x by A23, MESFUNC5:def 7; :: thesis: verum
end;
lim (R_EAL F) = R_EAL f by A18, A19, PARTFUN1:5;
hence lim (R_EAL F) = f by MESFUNC5:def 7; :: thesis: verum