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 & dom g = the carrier of X & dom h = the carrier of X & the carrier of X is empty ) by A3, FUNCT_2:def 1;
then ( h . x = 0 & f . x = 0 & g . x = 0 ) by FUNCT_1:def 4;
hence h . x = max (f . x),(g . x) ; :: thesis:

end;

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

take g ; :: thesis:
let x be Point of X; :: thesis:
( not x in A & the carrier of X <> {} ) by A4;
then f . x < g . x by A1;
hence g . x = max (f . x),(g . x) by XXREAL_0:def 10; :: thesis:

end;

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

take f ; :: thesis:
let x be Point of X; :: thesis:
( not x in B & the carrier of X <> {} ) by A5;
then g . x < f . x by A2;
hence f . x = max (f . x),(g . x) by XXREAL_0:def 10; :: thesis:

end;

suppose A6: ( 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 A6, Th53;
reconsider ff = f, gg = g as continuous Function of X',R ;
A7: ( dom ff = the carrier of X' & dom gg = the carrier of X' ) by FUNCT_2:def 1;
then A8: ( dom (ff | A') = A' & dom (gg | B') = B' ) by RELAT_1:91;
the carrier of (X' | A') = [#] (X' | A')
.= A' by PRE_TOPC:def 10 ;
then reconsider f' = ff | A' as continuous Function of (X' | A'),R by A8, FUNCT_2:def 1, RELSET_1:33, TOPMETR:10;
the carrier of (X' | B') = [#] (X' | B')
.= B' by PRE_TOPC:def 10 ;
then reconsider g' = gg | B' as continuous Function of (X' | B'),R by A8, FUNCT_2:def 1, RELSET_1:33, TOPMETR:10;
A9: 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 A10: X' | (A' \/ B') = X' | ([#] X')
.= TopStruct(# the carrier of X,the topology of X #) by TSEP_1:100 ;
A11: ( dom f' = A & dom g' = B ) by A7, RELAT_1:91;
A12: f' tolerates g'

proof

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

end;

then ( f' +* g' is continuous Function of (X' | (A' \/ B')),R & TopStruct(# the carrier of R,the topology of R #) = TopStruct(# the carrier of R,the topology of R #) ) by Th14;
then reconsider h = f' +* g' as continuous Function of X,R by A10, YELLOW12:36;
take h ; :: thesis:
let x be Point of X; :: thesis:
( x in the carrier of X' & ( x in A' or x in B' ) ) by A9, 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, A11, A12, FUNCT_1:72, FUNCT_4:14, FUNCT_4:16;
hence h . x = max (f . x),(g . x) by XXREAL_0:def 10; :: thesis:

end;