let a, b, c be Real; :: thesis: for f, g, F being Function of REAL,REAL st a <= b & b <= c & F = (f | [.a,b.]) +* (g | [.b,c.]) holds
F is Function of ['a,c'],REAL
let f, g, F be Function of REAL,REAL; :: thesis: ( a <= b & b <= c & F = (f | [.a,b.]) +* (g | [.b,c.]) implies F is Function of ['a,c'],REAL )
set g1 = f | [.a,b.];
set g2 = g | [.b,c.];
assume that
A1: ( a <= b & b <= c ) and
A2: F = (f | [.a,b.]) +* (g | [.b,c.]) ; :: thesis: F is Function of ['a,c'],REAL
Dg: dom F = (dom (f | [.a,b.])) \/ (dom (g | [.b,c.])) by FUNCT_4:def 1, A2
.= [.a,b.] \/ (dom (g | [.b,c.])) by FUNCT_2:def 1
.= [.a,b.] \/ [.b,c.] by FUNCT_2:def 1
.= [.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 . x in REAL by XREAL_0:def 1;
hence F is Function of ['a,c'],REAL by FUNCT_2:3, Dg; :: thesis: verum