let f, F, G be PartFunc of REAL,REAL; :: thesis: for I being non empty Interval st F is_antiderivative_of f,I & G is_antiderivative_of f,I holds
ex c being Real st
for x being Real st x in I holds
F . x = (G . x) + c
let I be non empty Interval; :: thesis: ( F is_antiderivative_of f,I & G is_antiderivative_of f,I implies ex c being Real st
for x being Real st x in I holds
F . x = (G . x) + c )
assume that
A1: F is_antiderivative_of f,I and
A2: G is_antiderivative_of f,I ; :: thesis: ex c being Real st
for x being Real st x in I holds
F . x = (G . x) + c
A3: inf I < sup I by A1, FDIFF_12:def 1;
reconsider J = ].(inf I),(sup I).[ as non empty Subset of REAL by A3, XXREAL_1:33;
( inf I is R_eal & sup I is R_eal ) by XXREAL_0:def 1;
then reconsider J = J as non empty open_interval Subset of REAL by MEASURE5:def 2;
J = ].(inf J),(sup J).[ by MEASURE6:16;
then inf J < sup J by XXREAL_1:28;
then ( F is_antiderivative_of f,J & G is_antiderivative_of f,J ) by A1, A2, Th42, FDIFF_12:2;
then consider c being Real such that
A4: for x being Real st x in J holds
F . x = (G . x) + c by Lm5;
take c ; :: thesis: for x being Real st x in I holds
F . x = (G . x) + c
( I c= dom F & I c= dom G ) by A1, A2, FDIFF_12:def 1;
then A5: ( I = dom (F | I) & I = dom (G | I) ) by RELAT_1:62;

per cases ( I is open_interval or I is closed_interval or I is left_open_interval or I is right_open_interval ) by MEASURE5:1;

suppose I is open_interval ; :: thesis: for x being Real st x in I holds
F . x = (G . x) + c

then I = ].(inf I),(sup I).[ by MEASURE6:16;
hence for x being Real st x in I holds
F . x = (G . x) + c by A4; :: thesis: verum

end;

suppose I is closed_interval ; :: thesis: for x being Real st x in I holds
F . x = (G . x) + c

then A6: I = [.(inf I),(sup I).] by MEASURE6:17;
then A7: ( inf I in I & sup I in I ) by A3, XXREAL_1:1;
A8: ( inf I = lower_bound I & sup I = upper_bound I ) by A3, A6, Th1, Th2, XXREAL_1:1;
then ( F | I is_continuous_in lower_bound I & F | I is_continuous_in upper_bound I & G | I is_continuous_in lower_bound I & G | I is_continuous_in upper_bound I ) by A5, A7, A1, A2, FDIFF_12:37, FCONT_1:def 2;
then A9: ( F | I is_Rcontinuous_in lower_bound I & F | I is_Lcontinuous_in upper_bound I & G | I is_Rcontinuous_in lower_bound I & G | I is_Lcontinuous_in upper_bound I ) by A5, A7, A8, FDIFF_12:26;
A10: for r being Real st r < upper_bound I holds
ex g being Real st
( r < g & g < upper_bound I & g in dom (F | I) )

proof

let r be Real; :: thesis: ( r < upper_bound I implies ex g being Real st
( r < g & g < upper_bound I & g in dom (F | I) ) )
assume A11: r < upper_bound I ; :: thesis: ex g being Real st
( r < g & g < upper_bound I & g in dom (F | I) )
set r1 = max (r,(lower_bound I));
consider g being Real such that
A12: ( max (r,(lower_bound I)) < g & g < upper_bound I ) by A11, A8, A3, XXREAL_0:29, XREAL_1:5;
take g ; :: thesis: ( r < g & g < upper_bound I & g in dom (F | I) )
( r <= max (r,(lower_bound I)) & lower_bound I <= max (r,(lower_bound I)) ) by XXREAL_0:25;
then ( r < g & lower_bound I < g ) by A12, XXREAL_0:2;
hence ( r < g & g < upper_bound I & g in dom (F | I) ) by A12, A8, A6, A5, XXREAL_1:1; :: thesis: verum

end;

then A13: ( F | I is_left_convergent_in upper_bound I & lim_left ((F | I),(upper_bound I)) = (F | I) . (upper_bound I) ) by A9, FDIFF_12:30;
A14: ( G | I is_left_convergent_in upper_bound I & lim_left ((G | I),(upper_bound I)) = (G | I) . (upper_bound I) ) by A5, A9, A10, FDIFF_12:30;
for e being Real st 0 < e holds
ex x2 being Real st
( x2 < upper_bound I & ( for x being Real st x2 < x & x < upper_bound I & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e ) )

proof

let e be Real; :: thesis: ( 0 < e implies ex x2 being Real st
( x2 < upper_bound I & ( for x being Real st x2 < x & x < upper_bound I & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e ) ) )
assume 0 < e ; :: thesis: ex x2 being Real st
( x2 < upper_bound I & ( for x being Real st x2 < x & x < upper_bound I & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e ) )
then consider x1 being Real such that
A15: ( x1 < upper_bound I & ( for x being Real st x1 < x & x < upper_bound I & x in dom (G | I) holds
|.(((G | I) . x) - ((G | I) . (upper_bound I))).| < e ) ) by A14, LIMFUNC2:41;
set x2 = max (x1,(lower_bound I));
take max (x1,(lower_bound I)) ; :: thesis: ( max (x1,(lower_bound I)) < upper_bound I & ( for x being Real st max (x1,(lower_bound I)) < x & x < upper_bound I & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e ) )
thus max (x1,(lower_bound I)) < upper_bound I by A15, A3, A8, XXREAL_0:29; :: thesis: for x being Real st max (x1,(lower_bound I)) < x & x < upper_bound I & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e
thus for x being Real st max (x1,(lower_bound I)) < x & x < upper_bound I & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e :: thesis: verum

proof

let x be Real; :: thesis: ( max (x1,(lower_bound I)) < x & x < upper_bound I & x in dom (F | I) implies |.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e )
assume that
A16: max (x1,(lower_bound I)) < x and
A17: x < upper_bound I and
A18: x in dom (F | I) ; :: thesis: |.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e
x1 <= max (x1,(lower_bound I)) by XXREAL_0:25;
then A19: x1 < x by A16, XXREAL_0:2;
lower_bound I <= max (x1,(lower_bound I)) by XXREAL_0:25;
then lower_bound I < x by A16, XXREAL_0:2;
then F . x = (G . x) + c by A4, A17, A8, XXREAL_1:4;
then (F | I) . x = (G . x) + c by A18, FUNCT_1:47;
then (F | I) . x = ((G | I) . x) + c by A18, A5, FUNCT_1:47;
then ((F | I) . x) - (((G | I) . (upper_bound I)) + c) = ((G | I) . x) - ((G | I) . (upper_bound I)) ;
hence |.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e by A15, A17, A18, A19, A5; :: thesis: verum

end;

end;

then (F | I) . (upper_bound I) = ((G | I) . (upper_bound I)) + c by A13, LIMFUNC2:41;
then A20: F . (upper_bound I) = ((G | I) . (upper_bound I)) + c by A6, A8, A3, XXREAL_1:1, FUNCT_1:49;
A21: for r being Real st lower_bound I < r holds
ex g being Real st
( g < r & lower_bound I < g & g in dom (F | I) )

proof

let r be Real; :: thesis: ( lower_bound I < r implies ex g being Real st
( g < r & lower_bound I < g & g in dom (F | I) ) )
assume A22: lower_bound I < r ; :: thesis: ex g being Real st
( g < r & lower_bound I < g & g in dom (F | I) )
set r1 = min (r,(upper_bound I));
consider g being Real such that
A23: ( lower_bound I < g & g < min (r,(upper_bound I)) ) by A22, A8, A3, XXREAL_0:21, XREAL_1:5;
take g ; :: thesis: ( g < r & lower_bound I < g & g in dom (F | I) )
( min (r,(upper_bound I)) <= r & min (r,(upper_bound I)) <= upper_bound I ) by XXREAL_0:17;
then ( g < r & g < upper_bound I ) by A23, XXREAL_0:2;
hence ( g < r & lower_bound I < g & g in dom (F | I) ) by A6, A8, A5, A23, XXREAL_1:1; :: thesis: verum

end;

then A24: ( F | I is_right_convergent_in lower_bound I & lim_right ((F | I),(lower_bound I)) = (F | I) . (lower_bound I) ) by A9, FDIFF_12:31;
A25: ( G | I is_right_convergent_in lower_bound I & lim_right ((G | I),(lower_bound I)) = (G | I) . (lower_bound I) ) by A5, A9, A21, FDIFF_12:31;
for e being Real st 0 < e holds
ex x2 being Real st
( lower_bound I < x2 & ( for x being Real st x < x2 & lower_bound I < x & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e ) )

proof

let e be Real; :: thesis: ( 0 < e implies ex x2 being Real st
( lower_bound I < x2 & ( for x being Real st x < x2 & lower_bound I < x & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e ) ) )
assume 0 < e ; :: thesis: ex x2 being Real st
( lower_bound I < x2 & ( for x being Real st x < x2 & lower_bound I < x & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e ) )
then consider x1 being Real such that
A26: ( lower_bound I < x1 & ( for x being Real st x < x1 & lower_bound I < x & x in dom (G | I) holds
|.(((G | I) . x) - ((G | I) . (lower_bound I))).| < e ) ) by A25, LIMFUNC2:42;
set x2 = min (x1,(upper_bound I));
take min (x1,(upper_bound I)) ; :: thesis: ( lower_bound I < min (x1,(upper_bound I)) & ( for x being Real st x < min (x1,(upper_bound I)) & lower_bound I < x & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e ) )
thus lower_bound I < min (x1,(upper_bound I)) by A26, A3, A8, XXREAL_0:21; :: thesis: for x being Real st x < min (x1,(upper_bound I)) & lower_bound I < x & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e
thus for x being Real st x < min (x1,(upper_bound I)) & lower_bound I < x & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e :: thesis: verum

proof

let x be Real; :: thesis: ( x < min (x1,(upper_bound I)) & lower_bound I < x & x in dom (F | I) implies |.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e )
assume that
A27: x < min (x1,(upper_bound I)) and
A28: lower_bound I < x and
A29: x in dom (F | I) ; :: thesis: |.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e
min (x1,(upper_bound I)) <= x1 by XXREAL_0:17;
then A30: x < x1 by A27, XXREAL_0:2;
min (x1,(upper_bound I)) <= upper_bound I by XXREAL_0:17;
then x < upper_bound I by A27, XXREAL_0:2;
then F . x = (G . x) + c by A4, A28, A8, XXREAL_1:4;
then (F | I) . x = (G . x) + c by A29, FUNCT_1:47;
then (F | I) . x = ((G | I) . x) + c by A29, A5, FUNCT_1:47;
then ((F | I) . x) - (((G | I) . (lower_bound I)) + c) = ((G | I) . x) - ((G | I) . (lower_bound I)) ;
hence |.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e by A26, A28, A29, A30, A5; :: thesis: verum

end;

end;

then (F | I) . (lower_bound I) = ((G | I) . (lower_bound I)) + c by A24, LIMFUNC2:42;
then A31: F . (lower_bound I) = ((G | I) . (lower_bound I)) + c by A6, A8, A3, XXREAL_1:1, FUNCT_1:49;

hereby :: thesis: verum

let x be Real; :: thesis: ( x in I implies F . x = (G . x) + c )
assume x in I ; :: thesis: F . x = (G . x) + c
then A32: ( lower_bound I <= x & x <= upper_bound I ) by A6, A8, XXREAL_1:1;

now :: thesis: ( x <> lower_bound I & x <> upper_bound I implies F . x = (G . x) + c )

assume ( x <> lower_bound I & x <> upper_bound I ) ; :: thesis: F . x = (G . x) + c
then ( lower_bound I < x & x < upper_bound I ) by A32, XXREAL_0:1;
hence F . x = (G . x) + c by A4, A8, XXREAL_1:4; :: thesis: verum

end;

hence F . x = (G . x) + c by A20, A31, A6, A8, A3, XXREAL_1:1, FUNCT_1:49; :: thesis: verum

end;

end;

suppose I is left_open_interval ; :: thesis: for x being Real st x in I holds
F . x = (G . x) + c

then A33: I = ].(inf I),(sup I).] by MEASURE6:19;
then A34: sup I in I by A3, XXREAL_1:2;
A35: sup I = upper_bound I by A3, A33, Th2, XXREAL_1:2;
then ( F | I is_continuous_in upper_bound I & G | I is_continuous_in upper_bound I ) by A5, A34, A1, A2, FDIFF_12:37, FCONT_1:def 2;
then A36: ( F | I is_Lcontinuous_in upper_bound I & G | I is_Lcontinuous_in upper_bound I ) by A5, A34, A35, FDIFF_12:26;
A37: for r being Real st r < upper_bound I holds
ex g being Real st
( r < g & g < upper_bound I & g in dom (F | I) )

proof

let r be Real; :: thesis: ( r < upper_bound I implies ex g being Real st
( r < g & g < upper_bound I & g in dom (F | I) ) )
assume A38: r < upper_bound I ; :: thesis: ex g being Real st
( r < g & g < upper_bound I & g in dom (F | I) )
set r1 = max (r,(inf I));
( max (r,(inf I)) is R_eal & upper_bound I is R_eal ) by XXREAL_0:def 1;
then consider g being Real such that
A39: ( max (r,(inf I)) < g & g < upper_bound I ) by A38, A35, A3, Th18, XXREAL_0:29;
take g ; :: thesis: ( r < g & g < upper_bound I & g in dom (F | I) )
( r <= max (r,(inf I)) & inf I <= max (r,(inf I)) ) by XXREAL_0:25;
then ( r < g & inf I < g ) by A39, XXREAL_0:2;
hence ( r < g & g < upper_bound I & g in dom (F | I) ) by A33, A35, A5, A39, XXREAL_1:2; :: thesis: verum

end;

then A40: ( F | I is_left_convergent_in upper_bound I & lim_left ((F | I),(upper_bound I)) = (F | I) . (upper_bound I) ) by A36, FDIFF_12:30;
A41: ( G | I is_left_convergent_in upper_bound I & lim_left ((G | I),(upper_bound I)) = (G | I) . (upper_bound I) ) by A5, A36, A37, FDIFF_12:30;
for e being Real st 0 < e holds
ex x2 being Real st
( x2 < upper_bound I & ( for x being Real st x2 < x & x < upper_bound I & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e ) )

proof

let e be Real; :: thesis: ( 0 < e implies ex x2 being Real st
( x2 < upper_bound I & ( for x being Real st x2 < x & x < upper_bound I & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e ) ) )
assume 0 < e ; :: thesis: ex x2 being Real st
( x2 < upper_bound I & ( for x being Real st x2 < x & x < upper_bound I & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e ) )
then consider x1 being Real such that
A42: ( x1 < upper_bound I & ( for x being Real st x1 < x & x < upper_bound I & x in dom (G | I) holds
|.(((G | I) . x) - ((G | I) . (upper_bound I))).| < e ) ) by A41, LIMFUNC2:41;
set x2 = max (x1,(inf I));
A43: ( x1 <= max (x1,(inf I)) & max (x1,(inf I)) < upper_bound I ) by A42, A3, A35, XXREAL_0:25, XXREAL_0:29;
( -infty < x1 & upper_bound I < +infty ) by XREAL_0:def 1, XXREAL_0:9, XXREAL_0:12;
then max (x1,(inf I)) in REAL by A43, XXREAL_0:14;
then reconsider x2 = max (x1,(inf I)) as Real ;
take x2 ; :: thesis: ( x2 < upper_bound I & ( for x being Real st x2 < x & x < upper_bound I & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e ) )
thus x2 < upper_bound I by A42, A3, A35, XXREAL_0:29; :: thesis: for x being Real st x2 < x & x < upper_bound I & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e
thus for x being Real st x2 < x & x < upper_bound I & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e :: thesis: verum

proof

let x be Real; :: thesis: ( x2 < x & x < upper_bound I & x in dom (F | I) implies |.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e )
assume that
A44: x2 < x and
A45: x < upper_bound I and
A46: x in dom (F | I) ; :: thesis: |.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e
x1 <= x2 by XXREAL_0:25;
then A47: x1 < x by A44, XXREAL_0:2;
inf I <= x2 by XXREAL_0:25;
then inf I < x by A44, XXREAL_0:2;
then F . x = (G . x) + c by A4, A45, A35, XXREAL_1:4;
then (F | I) . x = (G . x) + c by A46, FUNCT_1:47;
then (F | I) . x = ((G | I) . x) + c by A46, A5, FUNCT_1:47;
then ((F | I) . x) - (((G | I) . (upper_bound I)) + c) = ((G | I) . x) - ((G | I) . (upper_bound I)) ;
hence |.(((F | I) . x) - (((G | I) . (upper_bound I)) + c)).| < e by A42, A45, A46, A47, A5; :: thesis: verum

end;

end;

then (F | I) . (upper_bound I) = ((G | I) . (upper_bound I)) + c by A40, LIMFUNC2:41;
then A48: F . (upper_bound I) = ((G | I) . (upper_bound I)) + c by A33, A35, A3, XXREAL_1:2, FUNCT_1:49;

hereby :: thesis: verum

let x be Real; :: thesis: ( x in I implies F . x = (G . x) + c )
assume x in I ; :: thesis: F . x = (G . x) + c
then A49: ( inf I < x & x <= upper_bound I ) by A33, A35, XXREAL_1:2;

now :: thesis: ( x <> upper_bound I implies F . x = (G . x) + c )

assume x <> upper_bound I ; :: thesis: F . x = (G . x) + c
then ( inf I < x & x < upper_bound I ) by A49, XXREAL_0:1;
hence F . x = (G . x) + c by A4, A35, XXREAL_1:4; :: thesis: verum

end;

hence F . x = (G . x) + c by A48, A33, A35, A3, XXREAL_1:2, FUNCT_1:49; :: thesis: verum

end;

end;

suppose I is right_open_interval ; :: thesis: for x being Real st x in I holds
F . x = (G . x) + c

then A50: I = [.(inf I),(sup I).[ by MEASURE6:18;
then A51: inf I in I by A3, XXREAL_1:3;
A52: inf I = lower_bound I by A50, A3, Th1, XXREAL_1:3;
then ( F | I is_continuous_in lower_bound I & G | I is_continuous_in lower_bound I ) by A5, A51, A1, A2, FDIFF_12:37, FCONT_1:def 2;
then A53: ( F | I is_Rcontinuous_in lower_bound I & G | I is_Rcontinuous_in lower_bound I ) by A5, A51, A52, FDIFF_12:26;
A54: for r being Real st lower_bound I < r holds
ex g being Real st
( g < r & lower_bound I < g & g in dom (F | I) )

proof

let r be Real; :: thesis: ( lower_bound I < r implies ex g being Real st
( g < r & lower_bound I < g & g in dom (F | I) ) )
assume A55: lower_bound I < r ; :: thesis: ex g being Real st
( g < r & lower_bound I < g & g in dom (F | I) )
set r1 = min (r,(sup I));
( min (r,(sup I)) is R_eal & lower_bound I is R_eal ) by XXREAL_0:def 1;
then consider g being Real such that
A56: ( lower_bound I < g & g < min (r,(sup I)) ) by A55, A52, A3, Th18, XXREAL_0:21;
take g ; :: thesis: ( g < r & lower_bound I < g & g in dom (F | I) )
( min (r,(sup I)) <= r & min (r,(sup I)) <= sup I ) by XXREAL_0:17;
then ( g < r & g < sup I ) by A56, XXREAL_0:2;
hence ( g < r & lower_bound I < g & g in dom (F | I) ) by A52, A50, A5, A56, XXREAL_1:3; :: thesis: verum

end;

then A57: ( F | I is_right_convergent_in lower_bound I & lim_right ((F | I),(lower_bound I)) = (F | I) . (lower_bound I) ) by A53, FDIFF_12:31;
A58: ( G | I is_right_convergent_in lower_bound I & lim_right ((G | I),(lower_bound I)) = (G | I) . (lower_bound I) ) by A5, A53, A54, FDIFF_12:31;
for e being Real st 0 < e holds
ex x2 being Real st
( lower_bound I < x2 & ( for x being Real st x < x2 & lower_bound I < x & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e ) )

proof

let e be Real; :: thesis: ( 0 < e implies ex x2 being Real st
( lower_bound I < x2 & ( for x being Real st x < x2 & lower_bound I < x & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e ) ) )
assume 0 < e ; :: thesis: ex x2 being Real st
( lower_bound I < x2 & ( for x being Real st x < x2 & lower_bound I < x & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e ) )
then consider x1 being Real such that
A59: ( lower_bound I < x1 & ( for x being Real st x < x1 & lower_bound I < x & x in dom (G | I) holds
|.(((G | I) . x) - ((G | I) . (lower_bound I))).| < e ) ) by A58, LIMFUNC2:42;
set x2 = min (x1,(sup I));
A60: ( min (x1,(sup I)) <= x1 & lower_bound I < min (x1,(sup I)) ) by A59, A3, A52, XXREAL_0:17, XXREAL_0:21;
( x1 < +infty & lower_bound I > -infty ) by XREAL_0:def 1, XXREAL_0:9, XXREAL_0:12;
then min (x1,(sup I)) in REAL by A60, XXREAL_0:14;
then reconsider x2 = min (x1,(sup I)) as Real ;
take x2 ; :: thesis: ( lower_bound I < x2 & ( for x being Real st x < x2 & lower_bound I < x & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e ) )
thus lower_bound I < x2 by A59, A3, A52, XXREAL_0:21; :: thesis: for x being Real st x < x2 & lower_bound I < x & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e
thus for x being Real st x < x2 & lower_bound I < x & x in dom (F | I) holds
|.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e :: thesis: verum

proof

let x be Real; :: thesis: ( x < x2 & lower_bound I < x & x in dom (F | I) implies |.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e )
assume that
A61: x < x2 and
A62: lower_bound I < x and
A63: x in dom (F | I) ; :: thesis: |.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e
x2 <= x1 by XXREAL_0:17;
then A64: x < x1 by A61, XXREAL_0:2;
x2 <= sup I by XXREAL_0:17;
then x < sup I by A61, XXREAL_0:2;
then F . x = (G . x) + c by A4, A62, A52, XXREAL_1:4;
then (F | I) . x = (G . x) + c by A63, FUNCT_1:47;
then (F | I) . x = ((G | I) . x) + c by A63, A5, FUNCT_1:47;
then ((F | I) . x) - (((G | I) . (lower_bound I)) + c) = ((G | I) . x) - ((G | I) . (lower_bound I)) ;
hence |.(((F | I) . x) - (((G | I) . (lower_bound I)) + c)).| < e by A59, A62, A63, A64, A5; :: thesis: verum

end;

end;

then (F | I) . (lower_bound I) = ((G | I) . (lower_bound I)) + c by A57, LIMFUNC2:42;
then A65: F . (lower_bound I) = ((G | I) . (lower_bound I)) + c by A50, A52, A3, XXREAL_1:3, FUNCT_1:49;

hereby :: thesis: verum

let x be Real; :: thesis: ( x in I implies F . x = (G . x) + c )
assume x in I ; :: thesis: F . x = (G . x) + c
then A66: ( lower_bound I <= x & x < sup I ) by A50, A52, XXREAL_1:3;

now :: thesis: ( x <> lower_bound I implies F . x = (G . x) + c )

assume x <> lower_bound I ; :: thesis: F . x = (G . x) + c
then ( lower_bound I < x & x < sup I ) by A66, XXREAL_0:1;
hence F . x = (G . x) + c by A4, A52, XXREAL_1:4; :: thesis: verum

end;

hence F . x = (G . x) + c by A65, A50, A52, A3, XXREAL_1:3, FUNCT_1:49; :: thesis: verum

end;

end;

end;