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 ;
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 ;
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 ;
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 ;
for P being Subset of S st P is closed holds
h " P is closed
proof
reconsider M = [:F1,([#] Y):] as Subset of [:T,Y:] ;
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:]) ) )
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:]) )
proof
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 ;
hence x in g " P by ; :: thesis: verum
end;
assume A23: x in g " P ; :: thesis: x in (h " P) /\ ([#] [:T2,Y:])
then A24: x in dom g by FUNCT_1:def 7;
g . x in P by ;
then A25: h . x in P by ;
x in dom h by ;
then x in h " P by ;
hence x in (h " P) /\ ([#] [:T2,Y:]) by ; :: thesis: verum
end;
A26: for x being set st x in [#] [:T1,Y:] holds
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
now :: thesis: h . x = f . x
per cases ( x in [#] [:T2,Y:] or not x in [#] [:T2,Y:] ) ;
suppose A28: x in [#] [:T2,Y:] ; :: thesis: h . x = f . x
then x in ([#] [:T1,Y:]) /\ ([#] [:T2,Y:]) by ;
then f . x = g . x by A8;
hence h . x = f . x by ; :: thesis: verum
end;
suppose not x in [#] [:T2,Y:] ; :: thesis: h . x = f . x
hence h . x = f . x by ; :: thesis: verum
end;
end;
end;
hence h . x = f . x ; :: thesis: verum
end;
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:]) ) )
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:]) )
proof
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 ;
hence x in f " P by ; :: thesis: verum
end;
assume A32: x in f " P ; :: thesis: x in (h " P) /\ ([#] [:T1,Y:])
then x in dom f by FUNCT_1:def 7;
then A33: x in dom h by ;
f . x in P by ;
then h . x in P by ;
then x in h " P by ;
hence x in (h " P) /\ ([#] [:T1,Y:]) by ; :: thesis: verum
end;
then A34: (h " P) /\ ([#] [:T1,Y:]) = f " P by TARSKI:2;
the carrier of T2 is Subset of T by ;
then [#] [:T2,Y:] c= [#] [:T,Y:] by ;
then reconsider P2 = g " P as Subset of [:T,Y:] by XBOOLE_1:1;
the carrier of T1 is Subset of T by ;
then [#] [:T1,Y:] c= [#] [:T,Y:] by ;
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 ;
then A36: ex F01 being Subset of [:T,Y:] st
( F01 is closed & f " P = F01 /\ ([#] [:T1,Y:]) ) by ;
h " P = (h " P) /\ (([#] [:T1,Y:]) \/ ([#] [:T2,Y:])) by
.= ((h " P) /\ ([#] [:T1,Y:])) \/ ((h " P) /\ ([#] [:T2,Y:])) by XBOOLE_1:23 ;
then A37: h " P = (f " P) \/ (g " P) by ;
( M is closed & [#] [:T1,Y:] = [:F1,([#] Y):] ) by ;
then A38: P1 is closed by A36;
g " P is closed by ;
then A39: ex F02 being Subset of [:T,Y:] st
( F02 is closed & g " P = F02 /\ ([#] [:T2,Y:]) ) by ;
reconsider M = [:F2,([#] Y):] as Subset of [:T,Y:] ;
( M is closed & [#] [:T2,Y:] = [:F2,([#] Y):] ) by ;
then P2 is closed by A39;
hence h " P is closed by ; :: thesis: verum
end;
hence h is continuous by PRE_TOPC:def 6; :: thesis: verum