let T, T1, T2, S be non empty TopSpace; :: thesis: for f being Function of T1,S

for g being Function of T2,S st T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds

f . p = g . p ) holds

ex h being Function of T,S st

( h = f +* g & h is continuous )

let f be Function of T1,S; :: thesis: for g being Function of T2,S st T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds

f . p = g . p ) holds

ex h being Function of T,S st

( h = f +* g & h is continuous )

let g be Function of T2,S; :: thesis: ( T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds

f . p = g . p ) implies ex h being Function of T,S st

( h = f +* g & h is continuous ) )

assume that

A1: T1 is SubSpace of T and

A2: T2 is SubSpace of T and

A3: ([#] T1) \/ ([#] T2) = [#] T and

A4: T1 is compact and

A5: T2 is compact and

A6: T is T_2 and

A7: f is continuous and

A8: g is continuous and

A9: for p being set st p in ([#] T1) /\ ([#] T2) holds

f . p = g . p ; :: thesis: ex h being Function of T,S st

( h = f +* g & h is continuous )

set h = f +* g;

A10: dom g = [#] T2 by FUNCT_2:def 1;

A11: dom f = [#] T1 by FUNCT_2:def 1;

then A12: dom (f +* g) = the carrier of T by A3, A10, FUNCT_4:def 1;

rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;

then reconsider h = f +* g as Function of T,S by A12, FUNCT_2:2, XBOOLE_1:1;

take h ; :: thesis: ( h = f +* g & h is continuous )

thus h = f +* g ; :: thesis: h is continuous

for P being Subset of S st P is closed holds

h " P is closed

for g being Function of T2,S st T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds

f . p = g . p ) holds

ex h being Function of T,S st

( h = f +* g & h is continuous )

let f be Function of T1,S; :: thesis: for g being Function of T2,S st T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds

f . p = g . p ) holds

ex h being Function of T,S st

( h = f +* g & h is continuous )

let g be Function of T2,S; :: thesis: ( T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds

f . p = g . p ) implies ex h being Function of T,S st

( h = f +* g & h is continuous ) )

assume that

A1: T1 is SubSpace of T and

A2: T2 is SubSpace of T and

A3: ([#] T1) \/ ([#] T2) = [#] T and

A4: T1 is compact and

A5: T2 is compact and

A6: T is T_2 and

A7: f is continuous and

A8: g is continuous and

A9: for p being set st p in ([#] T1) /\ ([#] T2) holds

f . p = g . p ; :: thesis: ex h being Function of T,S st

( h = f +* g & h is continuous )

set h = f +* g;

A10: dom g = [#] T2 by FUNCT_2:def 1;

A11: dom f = [#] T1 by FUNCT_2:def 1;

then A12: dom (f +* g) = the carrier of T by A3, A10, FUNCT_4:def 1;

rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;

then reconsider h = f +* g as Function of T,S by A12, FUNCT_2:2, XBOOLE_1:1;

take h ; :: thesis: ( h = f +* g & h is continuous )

thus h = f +* g ; :: thesis: h is continuous

for P being Subset of S st P is closed holds

h " P is closed

proof

hence
h is continuous
; :: thesis: verum
let P be Subset of S; :: thesis: ( P is closed implies h " P is closed )

reconsider P3 = f " P as Subset of T1 ;

reconsider P4 = g " P as Subset of T2 ;

[#] T1 c= [#] T by A3, XBOOLE_1:7;

then reconsider P1 = f " P as Subset of T by XBOOLE_1:1;

[#] T2 c= [#] T by A3, XBOOLE_1:7;

then reconsider P2 = g " P as Subset of T by XBOOLE_1:1;

A13: dom h = (dom f) \/ (dom g) by FUNCT_4:def 1;

h . x = f . x

assume A28: P is closed ; :: thesis: h " P is closed

then P3 is closed by A7;

then P3 is compact by A4, COMPTS_1:8;

then A29: P1 is compact by A1, COMPTS_1:19;

P4 is closed by A8, A28;

then P4 is compact by A5, COMPTS_1:8;

then A30: P2 is compact by A2, COMPTS_1:19;

h " P = (h " P) /\ (([#] T1) \/ ([#] T2)) by A11, A10, A13, RELAT_1:132, XBOOLE_1:28

.= ((h " P) /\ ([#] T1)) \/ ((h " P) /\ ([#] T2)) by XBOOLE_1:23 ;

then h " P = (f " P) \/ (g " P) by A27, A14, TARSKI:2;

hence h " P is closed by A6, A29, A30; :: thesis: verum

end;reconsider P3 = f " P as Subset of T1 ;

reconsider P4 = g " P as Subset of T2 ;

[#] T1 c= [#] T by A3, XBOOLE_1:7;

then reconsider P1 = f " P as Subset of T by XBOOLE_1:1;

[#] T2 c= [#] T by A3, XBOOLE_1:7;

then reconsider P2 = g " P as Subset of T by XBOOLE_1:1;

A13: dom h = (dom f) \/ (dom g) by FUNCT_4:def 1;

A14: now :: thesis: for x being object holds

( ( x in (h " P) /\ ([#] T2) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] T2) ) )

A20:
for x being set st x in [#] T1 holds ( ( x in (h " P) /\ ([#] T2) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] T2) ) )

let x be object ; :: thesis: ( ( x in (h " P) /\ ([#] T2) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] T2) ) )

thus ( x in (h " P) /\ ([#] T2) implies x in g " P ) :: thesis: ( x in g " P implies x in (h " P) /\ ([#] T2) )

then A18: x in dom g by FUNCT_1:def 7;

g . x in P by A17, FUNCT_1:def 7;

then A19: h . x in P by A18, FUNCT_4:13;

x in dom h by A13, A18, XBOOLE_0:def 3;

then x in h " P by A19, FUNCT_1:def 7;

hence x in (h " P) /\ ([#] T2) by A17, XBOOLE_0:def 4; :: thesis: verum

end;thus ( x in (h " P) /\ ([#] T2) implies x in g " P ) :: thesis: ( x in g " P implies x in (h " P) /\ ([#] T2) )

proof

assume A17:
x in g " P
; :: thesis: x in (h " P) /\ ([#] T2)
assume A15:
x in (h " P) /\ ([#] T2)
; :: thesis: x in g " P

then x in h " P by XBOOLE_0:def 4;

then A16: h . x in P by FUNCT_1:def 7;

g . x = h . x by A10, A15, FUNCT_4:13;

hence x in g " P by A10, A15, A16, FUNCT_1:def 7; :: thesis: verum

end;then x in h " P by XBOOLE_0:def 4;

then A16: h . x in P by FUNCT_1:def 7;

g . x = h . x by A10, A15, FUNCT_4:13;

hence x in g " P by A10, A15, A16, FUNCT_1:def 7; :: thesis: verum

then A18: x in dom g by FUNCT_1:def 7;

g . x in P by A17, FUNCT_1:def 7;

then A19: h . x in P by A18, FUNCT_4:13;

x in dom h by A13, A18, XBOOLE_0:def 3;

then x in h " P by A19, FUNCT_1:def 7;

hence x in (h " P) /\ ([#] T2) by A17, XBOOLE_0:def 4; :: thesis: verum

h . x = f . x

proof

let x be set ; :: thesis: ( x in [#] T1 implies h . x = f . x )

assume A21: x in [#] T1 ; :: thesis: h . x = f . x

end;assume A21: x in [#] T1 ; :: thesis: h . x = f . x

now :: thesis: h . x = f . x

hence
h . x = f . x
; :: thesis: verumend;

now :: thesis: for x being object holds

( ( x in (h " P) /\ ([#] T1) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] T1) ) )

then A27:
(h " P) /\ ([#] T1) = f " P
by TARSKI:2;( ( x in (h " P) /\ ([#] T1) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] T1) ) )

let x be object ; :: thesis: ( ( x in (h " P) /\ ([#] T1) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] T1) ) )

thus ( x in (h " P) /\ ([#] T1) implies x in f " P ) :: thesis: ( x in f " P implies x in (h " P) /\ ([#] T1) )

then x in dom f by FUNCT_1:def 7;

then A26: x in dom h by A13, XBOOLE_0:def 3;

f . x in P by A25, FUNCT_1:def 7;

then h . x in P by A20, A25;

then x in h " P by A26, FUNCT_1:def 7;

hence x in (h " P) /\ ([#] T1) by A25, XBOOLE_0:def 4; :: thesis: verum

end;thus ( x in (h " P) /\ ([#] T1) implies x in f " P ) :: thesis: ( x in f " P implies x in (h " P) /\ ([#] T1) )

proof

assume A25:
x in f " P
; :: thesis: x in (h " P) /\ ([#] T1)
assume A23:
x in (h " P) /\ ([#] T1)
; :: thesis: x in f " P

then x in h " P by XBOOLE_0:def 4;

then A24: h . x in P by FUNCT_1:def 7;

f . x = h . x by A20, A23;

hence x in f " P by A11, A23, A24, FUNCT_1:def 7; :: thesis: verum

end;then x in h " P by XBOOLE_0:def 4;

then A24: h . x in P by FUNCT_1:def 7;

f . x = h . x by A20, A23;

hence x in f " P by A11, A23, A24, FUNCT_1:def 7; :: thesis: verum

then x in dom f by FUNCT_1:def 7;

then A26: x in dom h by A13, XBOOLE_0:def 3;

f . x in P by A25, FUNCT_1:def 7;

then h . x in P by A20, A25;

then x in h " P by A26, FUNCT_1:def 7;

hence x in (h " P) /\ ([#] T1) by A25, XBOOLE_0:def 4; :: thesis: verum

assume A28: P is closed ; :: thesis: h " P is closed

then P3 is closed by A7;

then P3 is compact by A4, COMPTS_1:8;

then A29: P1 is compact by A1, COMPTS_1:19;

P4 is closed by A8, A28;

then P4 is compact by A5, COMPTS_1:8;

then A30: P2 is compact by A2, COMPTS_1:19;

h " P = (h " P) /\ (([#] T1) \/ ([#] T2)) by A11, A10, A13, RELAT_1:132, XBOOLE_1:28

.= ((h " P) /\ ([#] T1)) \/ ((h " P) /\ ([#] T2)) by XBOOLE_1:23 ;

then h " P = (f " P) \/ (g " P) by A27, A14, TARSKI:2;

hence h " P is closed by A6, A29, A30; :: thesis: verum