let f, g be Function of REAL,REAL; :: thesis: ( f is continuous & g is continuous implies max (f,g) is continuous )
assume A1: f is continuous ; :: thesis: ( not g is continuous or max (f,g) is continuous )
assume A2: g is continuous ; :: thesis: max (f,g) is continuous
for x being Real holds (max (f,g)) . x = max ((f . x),(g . x))
proof
let x be Real; :: thesis: (max (f,g)) . x = max ((f . x),(g . x))
reconsider x = x as Element of REAL by XREAL_0:def 1;
(max (f,g)) . x = max ((f . x),(g . x)) by COUSIN2:def 2;
hence (max (f,g)) . x = max ((f . x),(g . x)) ; :: thesis: verum
end;
hence max (f,g) is continuous by FUZZY_5:16, A1, A2; :: thesis: verum