let a, b, c be Real; :: thesis: for f, g being Function of ['a,c'],REAL st a <= b & b <= c holds
(f | [.a,b.]) +* (g | [.b,c.]) is Function of ['a,c'],REAL
let f, g be Function of ['a,c'],REAL; :: thesis: ( a <= b & b <= c implies (f | [.a,b.]) +* (g | [.b,c.]) is Function of ['a,c'],REAL )
assume A1: ( a <= b & b <= c ) ; :: thesis: (f | [.a,b.]) +* (g | [.b,c.]) is Function of ['a,c'],REAL
set g1 = f | [.a,b.];
set g2 = g | [.b,c.];
set F = (f | [.a,b.]) +* (g | [.b,c.]);
B1: dom f = ['a,c'] by FUNCT_2:def 1
.= [.a,c.] by INTEGRA5:def 3, XXREAL_0:2, A1 ;
B2: dom g = ['a,c'] by FUNCT_2:def 1
.= [.a,c.] by INTEGRA5:def 3, XXREAL_0:2, A1 ;
D1: dom ((f | [.a,b.]) +* (g | [.b,c.])) = (dom (f | [.a,b.])) \/ (dom (g | [.b,c.])) by FUNCT_4:def 1
.= [.a,b.] \/ (dom (g | [.b,c.])) by B1, RELAT_1:62, XXREAL_1:34, A1
.= [.a,b.] \/ [.b,c.] by B2, RELAT_1:62, XXREAL_1:34, A1
.= [.a,c.] by XXREAL_1:165, A1
.= ['a,c'] by INTEGRA5:def 3, XXREAL_0:2, A1 ;
for x being object st x in ['a,c'] holds
((f | [.a,b.]) +* (g | [.b,c.])) . x in REAL by XREAL_0:def 1;
hence (f | [.a,b.]) +* (g | [.b,c.]) is Function of ['a,c'],REAL by FUNCT_2:3, D1; :: thesis: verum