let a, b, c be Real; :: thesis: for f, g, F being Function of REAL,REAL st a <= b & b <= c & f is continuous & g is continuous & F = (f | [.a,b.]) +* (g | [.b,c.]) & f . b = g . b holds
F is continuous
let f, g, F be Function of REAL,REAL; :: thesis: ( a <= b & b <= c & f is continuous & g is continuous & F = (f | [.a,b.]) +* (g | [.b,c.]) & f . b = g . b implies F is continuous )
assume that
A1: ( a <= b & b <= c ) and
A2: ( f is continuous & g is continuous ) and
A3: F = (f | [.a,b.]) +* (g | [.b,c.]) and
A4: f . b = g . b ; :: thesis: F is continuous
F = F | [.a,c.] by Th25, A1, A3;
hence F is continuous by Lm22b1, A1, A2, A3, A4; :: thesis: verum