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

for g being Function of [:T2,Y:],S

for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds

f . p = g . p ) holds

ex h being Function of [:T,Y:],S st

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

let f be Function of [:T1,Y:],S; :: thesis: for g being Function of [:T2,Y:],S

for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds

f . p = g . p ) holds

ex h being Function of [:T,Y:],S st

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

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

f . p = g . p ) holds

ex h being Function of [:T,Y:],S st

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

let F1, F2 be closed Subset of T; :: thesis: ( T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds

f . p = g . p ) implies ex h being Function of [:T,Y:],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: F1 = [#] T1 and

A4: F2 = [#] T2 and

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

A6: f is continuous and

A7: g is continuous and

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

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

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

A9: dom f = the carrier of [:T1,Y:] by FUNCT_2:def 1;

A10: Y is SubSpace of Y by TSEP_1:2;

then A11: [:T2,Y:] is SubSpace of [:T,Y:] by A2, BORSUK_3:21;

set h = f +* g;

A12: the carrier of [:T2,Y:] = [: the carrier of T2, the carrier of Y:] by BORSUK_1:def 2;

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

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

A15: dom g = the carrier of [:T2,Y:] by FUNCT_2:def 1;

A16: the carrier of [:T1,Y:] = [: the carrier of T1, the carrier of Y:] by BORSUK_1:def 2;

then A17: dom (f +* g) = [: the carrier of T, the carrier of Y:] by A5, A12, A9, A15, A13, ZFMISC_1:97;

A18: the carrier of [:T,Y:] = [: the carrier of T, the carrier of Y:] by BORSUK_1:def 2;

then reconsider h = f +* g as Function of [:T,Y:],S by A17, A14, FUNCT_2:2, XBOOLE_1:1;

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

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

A19: [:T1,Y:] is SubSpace of [:T,Y:] by A1, A10, BORSUK_3:21;

for P being Subset of S st P is closed holds

h " P is closed

for g being Function of [:T2,Y:],S

for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds

f . p = g . p ) holds

ex h being Function of [:T,Y:],S st

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

let f be Function of [:T1,Y:],S; :: thesis: for g being Function of [:T2,Y:],S

for F1, F2 being closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds

f . p = g . p ) holds

ex h being Function of [:T,Y:],S st

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

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

f . p = g . p ) holds

ex h being Function of [:T,Y:],S st

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

let F1, F2 be closed Subset of T; :: thesis: ( T1 is SubSpace of T & T2 is SubSpace of T & F1 = [#] T1 & F2 = [#] T2 & ([#] T1) \/ ([#] T2) = [#] T & f is continuous & g is continuous & ( for p being set st p in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) holds

f . p = g . p ) implies ex h being Function of [:T,Y:],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: F1 = [#] T1 and

A4: F2 = [#] T2 and

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

A6: f is continuous and

A7: g is continuous and

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

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

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

A9: dom f = the carrier of [:T1,Y:] by FUNCT_2:def 1;

A10: Y is SubSpace of Y by TSEP_1:2;

then A11: [:T2,Y:] is SubSpace of [:T,Y:] by A2, BORSUK_3:21;

set h = f +* g;

A12: the carrier of [:T2,Y:] = [: the carrier of T2, the carrier of Y:] by BORSUK_1:def 2;

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

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

A15: dom g = the carrier of [:T2,Y:] by FUNCT_2:def 1;

A16: the carrier of [:T1,Y:] = [: the carrier of T1, the carrier of Y:] by BORSUK_1:def 2;

then A17: dom (f +* g) = [: the carrier of T, the carrier of Y:] by A5, A12, A9, A15, A13, ZFMISC_1:97;

A18: the carrier of [:T,Y:] = [: the carrier of T, the carrier of Y:] by BORSUK_1:def 2;

then reconsider h = f +* g as Function of [:T,Y:],S by A17, A14, FUNCT_2:2, XBOOLE_1:1;

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

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

A19: [:T1,Y:] is SubSpace of [:T,Y:] by A1, A10, BORSUK_3:21;

for P being Subset of S st P is closed holds

h " P is closed

proof

hence
h is continuous
by PRE_TOPC:def 6; :: thesis: verum
reconsider M = [:F1,([#] Y):] as Subset of [:T,Y:] ;

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

h . x = f . x

the carrier of T2 is Subset of T by A2, TSEP_1:1;

then [#] [:T2,Y:] c= [#] [:T,Y:] by A18, A12, ZFMISC_1:95;

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

the carrier of T1 is Subset of T by A1, TSEP_1:1;

then [#] [:T1,Y:] c= [#] [:T,Y:] by A18, A16, ZFMISC_1:95;

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

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

then f " P is closed by A6, PRE_TOPC:def 6;

then A36: ex F01 being Subset of [:T,Y:] st

( F01 is closed & f " P = F01 /\ ([#] [:T1,Y:]) ) by A19, PRE_TOPC:13;

h " P = (h " P) /\ (([#] [:T1,Y:]) \/ ([#] [:T2,Y:])) by A18, A9, A15, A13, A17, XBOOLE_1:28

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

then A37: h " P = (f " P) \/ (g " P) by A34, A20, TARSKI:2;

( M is closed & [#] [:T1,Y:] = [:F1,([#] Y):] ) by A3, Th15, BORSUK_3:1;

then A38: P1 is closed by A36;

g " P is closed by A7, A35, PRE_TOPC:def 6;

then A39: ex F02 being Subset of [:T,Y:] st

( F02 is closed & g " P = F02 /\ ([#] [:T2,Y:]) ) by A11, PRE_TOPC:13;

reconsider M = [:F2,([#] Y):] as Subset of [:T,Y:] ;

( M is closed & [#] [:T2,Y:] = [:F2,([#] Y):] ) by A4, Th15, BORSUK_3:1;

then P2 is closed by A39;

hence h " P is closed by A37, A38; :: thesis: verum

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

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

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

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

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

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

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

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

then A25: h . x in P by A24, FUNCT_4:13;

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

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

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

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

proof

assume A23:
x in g " P
; :: thesis: x in (h " P) /\ ([#] [:T2,Y:])
assume A21:
x in (h " P) /\ ([#] [:T2,Y:])
; :: thesis: x in g " P

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

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

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

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

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

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

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

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

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

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

then A25: h . x in P by A24, FUNCT_4:13;

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

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

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

h . x = f . x

proof

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

assume A27: x in [#] [:T1,Y:] ; :: thesis: h . x = f . x

end;assume A27: x in [#] [:T1,Y:] ; :: 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,Y:]) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] [:T1,Y:]) ) )

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

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

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

then x in dom f by FUNCT_1:def 7;

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

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

then h . x in P by A26, A32;

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

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

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

proof

assume A32:
x in f " P
; :: thesis: x in (h " P) /\ ([#] [:T1,Y:])
assume A29:
x in (h " P) /\ ([#] [:T1,Y:])
; :: thesis: x in f " P

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

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

x in [#] [:T1,Y:] by A29;

then A31: x in dom f by FUNCT_2:def 1;

f . x = h . x by A26, A29;

hence x in f " P by A30, A31, FUNCT_1:def 7; :: thesis: verum

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

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

x in [#] [:T1,Y:] by A29;

then A31: x in dom f by FUNCT_2:def 1;

f . x = h . x by A26, A29;

hence x in f " P by A30, A31, FUNCT_1:def 7; :: thesis: verum

then x in dom f by FUNCT_1:def 7;

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

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

then h . x in P by A26, A32;

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

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

the carrier of T2 is Subset of T by A2, TSEP_1:1;

then [#] [:T2,Y:] c= [#] [:T,Y:] by A18, A12, ZFMISC_1:95;

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

the carrier of T1 is Subset of T by A1, TSEP_1:1;

then [#] [:T1,Y:] c= [#] [:T,Y:] by A18, A16, ZFMISC_1:95;

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

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

then f " P is closed by A6, PRE_TOPC:def 6;

then A36: ex F01 being Subset of [:T,Y:] st

( F01 is closed & f " P = F01 /\ ([#] [:T1,Y:]) ) by A19, PRE_TOPC:13;

h " P = (h " P) /\ (([#] [:T1,Y:]) \/ ([#] [:T2,Y:])) by A18, A9, A15, A13, A17, XBOOLE_1:28

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

then A37: h " P = (f " P) \/ (g " P) by A34, A20, TARSKI:2;

( M is closed & [#] [:T1,Y:] = [:F1,([#] Y):] ) by A3, Th15, BORSUK_3:1;

then A38: P1 is closed by A36;

g " P is closed by A7, A35, PRE_TOPC:def 6;

then A39: ex F02 being Subset of [:T,Y:] st

( F02 is closed & g " P = F02 /\ ([#] [:T2,Y:]) ) by A11, PRE_TOPC:13;

reconsider M = [:F2,([#] Y):] as Subset of [:T,Y:] ;

( M is closed & [#] [:T2,Y:] = [:F2,([#] Y):] ) by A4, Th15, BORSUK_3:1;

then P2 is closed by A39;

hence h " P is closed by A37, A38; :: thesis: verum