let x, y be PartFunc of REAL,REAL; :: thesis: for a, b being Real st a < b & [.a,b.] c= dom x & [.a,b.] c= dom y & x is continuous & y is continuous & ( for t being Real st t in ].a,b.[ holds
x . t = y . t ) holds
x | [.a,b.] = y | [.a,b.]
let a, b be Real; :: thesis: ( a < b & [.a,b.] c= dom x & [.a,b.] c= dom y & x is continuous & y is continuous & ( for t being Real st t in ].a,b.[ holds
x . t = y . t ) implies x | [.a,b.] = y | [.a,b.] )
assume that
A1: ( a < b & [.a,b.] c= dom x & [.a,b.] c= dom y & x is continuous & y is continuous ) and
A2: for t being Real st t in ].a,b.[ holds
x . t = y . t ; :: thesis: x | [.a,b.] = y | [.a,b.]
A3: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then A4: ].a,b.[ c= ['a,b'] by Lm1;
set z = a + ((b - a) / 2);
A5: 0 < b - a by A1, XREAL_1:50;
then (b - a) / 2 < b - a by XREAL_1:216;
then A7: a + ((b - a) / 2) < (b - a) + a by XREAL_1:8;
deffunc H₁( Nat) -> Element of REAL = In ((((b - a) / 2) / ($1 + 1)),REAL);
consider Sn being Function of NAT,REAL such that
A8: for x being Element of NAT holds Sn . x = H₁(x) from FUNCT_2:sch 4();
A9: for n being Nat holds Sn . n = ((b - a) / 2) / (n + 1)

proof

let n be Nat; :: thesis: Sn . n = ((b - a) / 2) / (n + 1)
n in NAT by ORDINAL1:def 12;
hence Sn . n = In ((((b - a) / 2) / (n + 1)),REAL) by A8
.= ((b - a) / 2) / (n + 1) ;
:: thesis: verum

end;

then A10: ( Sn is convergent & lim Sn = 0 ) by SEQ_4:31;
consider Sa being constant Function of NAT,REAL such that
A12: for x being Nat holds Sa . x = a by LmX;
A15: Sa . 0 = a by A12;
set S0 = Sa + Sn;
( Sa + Sn is convergent & lim (Sa + Sn) = (lim Sa) + (lim Sn) ) by A10, SEQ_2:6;
then A16: lim (Sa + Sn) = a by A10, A15, SEQ_4:25;
a in [.a,b.] by A1;
then A17: ( x is_continuous_in a & y is_continuous_in a ) by A1;
A18: rng (Sa + Sn) c= ].a,b.[

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Sa + Sn) or y in ].a,b.[ )
assume y in rng (Sa + Sn) ; :: thesis: y in ].a,b.[
then consider n being object such that
A19: ( n in dom (Sa + Sn) & y = (Sa + Sn) . n ) by FUNCT_1:def 3;
reconsider n = n as Nat by A19;
A20: y = (Sa . n) + (Sn . n) by A19, SEQ_1:7
.= a + (Sn . n) by A12
.= a + (((b - a) / 2) / (n + 1)) by A9 ;
A21: a + 0 < a + (((b - a) / 2) / (n + 1)) by A5, XREAL_1:8;
1 + 0 <= n + 1 by XREAL_1:7;
then ((b - a) / 2) / (n + 1) <= ((b - a) / 2) / 1 by A5, XREAL_1:118;
then a + (((b - a) / 2) / (n + 1)) <= a + ((b - a) / 2) by XREAL_1:7;
then a + (((b - a) / 2) / (n + 1)) < b by A7, XXREAL_0:2;
hence y in ].a,b.[ by A20, A21; :: thesis: verum

end;

then A23: ( rng (Sa + Sn) c= dom x & rng (Sa + Sn) c= dom y ) by A1, A3, A4;
then A24: ( x /* (Sa + Sn) is convergent & x . a = lim (x /* (Sa + Sn)) & y /* (Sa + Sn) is convergent & y . a = lim (y /* (Sa + Sn)) ) by A10, A16, A17;
for n being Nat holds (x /* (Sa + Sn)) . n = (y /* (Sa + Sn)) . n

proof

let n be Nat; :: thesis: (x /* (Sa + Sn)) . n = (y /* (Sa + Sn)) . n
A25: n in NAT by ORDINAL1:def 12;
then A26: ( (x /* (Sa + Sn)) . n = x . ((Sa + Sn) . n) & (y /* (Sa + Sn)) . n = y . ((Sa + Sn) . n) ) by A23, FUNCT_2:108;
(Sa + Sn) . n in ].a,b.[ by A18, A25, FUNCT_2:112;
hence (x /* (Sa + Sn)) . n = (y /* (Sa + Sn)) . n by A2, A26; :: thesis: verum

end;

then A27: x /* (Sa + Sn) = y /* (Sa + Sn) ;
consider Sb being constant Function of NAT,REAL such that
A29: for x being Nat holds Sb . x = b by LmX;
Sb . 0 = b by A29;
then A31: ( Sb is convergent & lim Sb = b ) by SEQ_4:25;
set S1 = Sb - Sn;
A32: lim (Sb - Sn) = b - 0 by A10, A31, SEQ_2:12
.= b ;
b in [.a,b.] by A1;
then A33: ( x is_continuous_in b & y is_continuous_in b ) by A1;
A34: rng (Sb - Sn) c= ].a,b.[

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Sb - Sn) or y in ].a,b.[ )
assume y in rng (Sb - Sn) ; :: thesis: y in ].a,b.[
then consider n being object such that
A35: ( n in dom (Sb - Sn) & y = (Sb - Sn) . n ) by FUNCT_1:def 3;
reconsider n = n as Nat by A35;
A36: y = (Sb . n) + ((- Sn) . n) by A35, SEQ_1:7
.= (Sb . n) + (- (Sn . n)) by SEQ_1:10
.= b - (Sn . n) by A29
.= b - (((b - a) / 2) / (n + 1)) by A9 ;
A37: b - (((b - a) / 2) / (n + 1)) < b - 0 by A5, XREAL_1:15;
1 + 0 <= n + 1 by XREAL_1:7;
then ((b - a) / 2) / (n + 1) <= ((b - a) / 2) / 1 by A5, XREAL_1:118;
then A38: b - ((b - a) / 2) <= b - (((b - a) / 2) / (n + 1)) by XREAL_1:13;
a + 0 < a + ((b - a) / 2) by A5, XREAL_1:8;
then a < b - (((b - a) / 2) / (n + 1)) by A38, XXREAL_0:2;
hence y in ].a,b.[ by A36, A37; :: thesis: verum

end;

then A40: ( rng (Sb - Sn) c= dom x & rng (Sb - Sn) c= dom y ) by A1, A3, A4;
then A41: ( x /* (Sb - Sn) is convergent & x . b = lim (x /* (Sb - Sn)) & y /* (Sb - Sn) is convergent & y . b = lim (y /* (Sb - Sn)) ) by A10, A32, A33;
for n being Nat holds (x /* (Sb - Sn)) . n = (y /* (Sb - Sn)) . n

proof

let n be Nat; :: thesis: (x /* (Sb - Sn)) . n = (y /* (Sb - Sn)) . n
A42: n in NAT by ORDINAL1:def 12;
then A43: ( (x /* (Sb - Sn)) . n = x . ((Sb - Sn) . n) & (y /* (Sb - Sn)) . n = y . ((Sb - Sn) . n) ) by A40, FUNCT_2:108;
(Sb - Sn) . n in ].a,b.[ by A34, A42, FUNCT_2:112;
hence (x /* (Sb - Sn)) . n = (y /* (Sb - Sn)) . n by A2, A43; :: thesis: verum

end;

then A44: x /* (Sb - Sn) = y /* (Sb - Sn) ;
A45: dom (x | [.a,b.]) = [.a,b.] by A1, RELAT_1:62;
A46: dom (y | [.a,b.]) = [.a,b.] by A1, RELAT_1:62;
for t being object st t in dom (x | [.a,b.]) holds
(x | [.a,b.]) . t = (y | [.a,b.]) . t

proof

let s be object ; :: thesis: ( s in dom (x | [.a,b.]) implies (x | [.a,b.]) . s = (y | [.a,b.]) . s )
assume A47: s in dom (x | [.a,b.]) ; :: thesis: (x | [.a,b.]) . s = (y | [.a,b.]) . s
then reconsider t = s as Real ;
t in [.a,b.] by A1, A47, RELAT_1:62;
then ex r being Real st
( t = r & a <= r & r <= b ) ;

per cases then ( t = a or ( a < t & t < b ) or t = b ) by XXREAL_0:1;

suppose A50: t = a ; :: thesis: (x | [.a,b.]) . s = (y | [.a,b.]) . s

thus (x | [.a,b.]) . s = x . t by A45, A47, FUNCT_1:49
.= (y | [.a,b.]) . s by A24, A27, A45, A47, A50, FUNCT_1:49 ; :: thesis: verum

end;

suppose ( a < t & t < b ) ; :: thesis: (x | [.a,b.]) . s = (y | [.a,b.]) . s

then A51: t in ].a,b.[ ;
thus (x | [.a,b.]) . s = x . t by A45, A47, FUNCT_1:49
.= y . t by A2, A51
.= (y | [.a,b.]) . s by A45, A47, FUNCT_1:49 ; :: thesis: verum

end;

suppose A52: t = b ; :: thesis: (x | [.a,b.]) . s = (y | [.a,b.]) . s

thus (x | [.a,b.]) . s = x . t by A45, A47, FUNCT_1:49
.= (y | [.a,b.]) . s by A41, A44, A45, A47, A52, FUNCT_1:49 ; :: thesis: verum

end;

end;

end;

hence x | [.a,b.] = y | [.a,b.] by A1, RELAT_1:62, A46, FUNCT_1:2; :: thesis: verum