let X be TopSpace; :: thesis:
let R be non empty SubSpace of R^1 ; :: thesis:
let f, g be continuous Function of X,R; :: thesis:
defpred S₁[ set ] means f . $1 >= g . $1;
consider A being Subset of X such that
A1: for a being set holds
( a in A iff ( a in the carrier of X & S₁[a] ) ) from SUBSET_1:sch 1();
defpred S₂[ set ] means f . $1 <= g . $1;
consider B being Subset of X such that
A2: for a being set holds
( a in B iff ( a in the carrier of X & S₂[a] ) ) from SUBSET_1:sch 1();

per cases ;

suppose A3: X is empty ; :: thesis:

consider h being continuous Function of X,R;
take h ; :: thesis:
let x be Point of X; :: thesis:
dom f = the carrier of X by FUNCT_2:def 1;
then A4: f . x = 0 by A3, FUNCT_1:def 4;
dom g = the carrier of X by FUNCT_2:def 1;
then A5: g . x = 0 by A3, FUNCT_1:def 4;
dom h = the carrier of X by FUNCT_2:def 1;
hence h . x = max (f . x),(g . x) by A3, A4, A5, FUNCT_1:def 4; :: thesis:

end;

suppose A6: ( not X is empty & A is empty ) ; :: thesis:

take g ; :: thesis:
let x be Point of X; :: thesis:
f . x < g . x by A6, A1;
hence g . x = max (f . x),(g . x) by XXREAL_0:def 10; :: thesis:

end;

suppose A7: ( not X is empty & B is empty ) ; :: thesis:

take f ; :: thesis:
let x be Point of X; :: thesis:
g . x < f . x by A7, A2;
hence f . x = max (f . x),(g . x) by XXREAL_0:def 10; :: thesis:

end;

suppose A8: ( not X is empty & not A is empty & not B is empty ) ; :: thesis:

then reconsider X' = X as non empty TopSpace ;
for x being Point of X' holds
( ( x in A implies f . x >= g . x ) & ( f . x >= g . x implies x in A ) & ( x in B implies f . x <= g . x ) & ( f . x <= g . x implies x in B ) ) by A1, A2;
then reconsider A' = A, B' = B as non empty closed Subset of X' by A8, Th53;
reconsider ff = f, gg = g as continuous Function of X',R ;
A9: the carrier of (X' | A') = [#] (X' | A')
.= A' by PRE_TOPC:def 10 ;
A10: dom ff = the carrier of X' by FUNCT_2:def 1;
then dom (ff | A') = A' by RELAT_1:91;
then reconsider f' = ff | A' as continuous Function of (X' | A'),R by A9, FUNCT_2:def 1, RELSET_1:33, TOPMETR:10;
A11: the carrier of (X' | B') = [#] (X' | B')
.= B' by PRE_TOPC:def 10 ;
A12: dom gg = the carrier of X' by FUNCT_2:def 1;
then dom (gg | B') = B' by RELAT_1:91;
then reconsider g' = gg | B' as continuous Function of (X' | B'),R by A11, FUNCT_2:def 1, RELSET_1:33, TOPMETR:10;
A13: dom g' = B by A12, RELAT_1:91;
A14: A' \/ B' = the carrier of X'

proof

thus A' \/ B' c= the carrier of X' ; :: according to XBOOLE_0:def 10 :: thesis:
let a be set ; :: according to TARSKI:def 3 :: thesis:
( f . a >= g . a or f . a <= g . a ) ;
then ( not a in the carrier of X or a in A' or a in B' ) by A1, A2;
hence ( not a in the carrier of X' or a in A' \/ B' ) by XBOOLE_0:def 3; :: thesis:

end;

then A15: X' | (A' \/ B') = X' | ([#] X')
.= TopStruct(# the carrier of X,the topology of X #) by TSEP_1:100 ;
A16: TopStruct(# the carrier of R,the topology of R #) = TopStruct(# the carrier of R,the topology of R #) ;
A17: dom f' = A by A10, RELAT_1:91;
A18: f' tolerates g'

proof

let a be set ; :: according to PARTFUN1:def 6 :: thesis:
assume A19: a in (dom f') /\ (dom g') ; :: thesis:
then A20: a in A by A17, XBOOLE_0:def 4;
then A21: f . a >= g . a by A1;
A22: a in B by A19, A13, XBOOLE_0:def 4;
then f . a <= g . a by A2;
then f . a = g . a by A21, XXREAL_0:1;
hence f' . a = g . a by A20, FUNCT_1:72
.= g' . a by A22, FUNCT_1:72 ;
:: thesis:

end;

then f' +* g' is continuous Function of (X' | (A' \/ B')),R by Th14;
then reconsider h = f' +* g' as continuous Function of X,R by A16, A15, YELLOW12:36;
take h ; :: thesis:
let x be Point of X; :: thesis:
( x in A' or x in B' ) by A14, XBOOLE_0:def 3;
then ( ( x in A' & f . x >= g . x & h . x = f' . x & f . x = f' . x ) or ( x in B' & f . x <= g . x & h . x = g' . x & g . x = g' . x ) ) by A1, A2, A17, A13, A18, FUNCT_1:72, FUNCT_4:14, FUNCT_4:16;
hence h . x = max (f . x),(g . x) by XXREAL_0:def 10; :: thesis:

end;