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 = F | [.a,c.]
let f, g, F be Function of REAL,REAL; :: thesis: ( a <= b & b <= c & F = (f | [.a,b.]) +* (g | [.b,c.]) implies F = F | [.a,c.] )
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 = F | [.a,c.]
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 ;
hence F = F | [.a,c.] ; :: thesis: verum