let c be Real; :: thesis: for f, g being Function of REAL,REAL st f is continuous & g is continuous & f . c = g . c holds
(f | ].-infty,c.]) +* (g | [.c,+infty.[) is continuous Function of REAL,REAL
let f, g be Function of REAL,REAL; :: thesis: ( f is continuous & g is continuous & f . c = g . c implies (f | ].-infty,c.]) +* (g | [.c,+infty.[) is continuous Function of REAL,REAL )
assume that
A1: ( f is continuous & g is continuous ) and
A2: f . c = g . c ; :: thesis: (f | ].-infty,c.]) +* (g | [.c,+infty.[) is continuous Function of REAL,REAL
reconsider F = (f | ].-infty,c.]) +* (g | [.c,+infty.[) as PartFunc of REAL,REAL by FUZZY_7:12;
( ].-infty,c.] c= REAL & [.c,+infty.[ c= REAL ) ;
then ( ].-infty,c.] c= dom f & [.c,+infty.[ c= dom g ) by FUNCT_2:def 1;
hence (f | ].-infty,c.]) +* (g | [.c,+infty.[) is continuous Function of REAL,REAL by Th1, A2, A1, FUZZY_7:12; :: thesis: verum