let T, S be non empty TopSpace; :: thesis: for X being set
for T1, T2 being SubSpace of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = X & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f | X tolerates g | X holds
f +* g is continuous Function of T,S
let X be set ; :: thesis: for T1, T2 being SubSpace of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = X & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f | X tolerates g | X holds
f +* g is continuous Function of T,S
let T1, T2 be SubSpace of T; :: thesis: for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = X & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f | X tolerates g | X holds
f +* g is continuous Function of T,S
let f be Function of T1,S; :: thesis: for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = X & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f | X tolerates g | X holds
f +* g is continuous Function of T,S
let g be Function of T2,S; :: thesis: ( ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = X & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f | X tolerates g | X implies f +* g is continuous Function of T,S )
assume that
A1: ([#] T1) \/ ([#] T2) = [#] T and
A2: ([#] T1) /\ ([#] T2) = X and
A3: T1 is compact and
A4: T2 is compact and
A5: T is T_2 and
A6: f is continuous and
A7: g is continuous and
A8: f | X tolerates g | X ; :: thesis: f +* g is continuous Function of T,S
set h = f +* g;
A9: dom g = [#] T2 by FUNCT_2:def 1;
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then A10: rng (f +* g) c= the carrier of S by XBOOLE_1:1;
A11: dom f = [#] T1 by FUNCT_2:def 1;
then dom (f +* g) = the carrier of T by A1, A9, FUNCT_4:def 1;
then reconsider h = f +* g as Function of T,S by A10, FUNCT_2:def 1, RELSET_1:4;
for P being Subset of S st P is closed holds
h " P is closed
proof
let P be Subset of S; :: thesis: ( P is closed implies h " P is closed )
[#] T1 c= [#] T by A1, XBOOLE_1:7;
then reconsider P1 = f " P as Subset of T by XBOOLE_1:1;
[#] T2 c= [#] T by A1, XBOOLE_1:7;
then reconsider P2 = g " P as Subset of T by XBOOLE_1:1;
A12: dom h = (dom f) \/ (dom g) by FUNCT_4:def 1;
A13: 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) ) )
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) )
proof
assume A14: x in (h " P) /\ ([#] T2) ; :: thesis: x in g " P
then x in h " P by XBOOLE_0:def 4;
then A15: h . x in P by FUNCT_1:def 7;
g . x = h . x by A9, A14, FUNCT_4:13;
hence x in g " P by A9, A14, A15, FUNCT_1:def 7; :: thesis: verum
end;
assume A16: x in g " P ; :: thesis: x in (h " P) /\ ([#] T2)
then A17: x in dom g by FUNCT_1:def 7;
g . x in P by A16, FUNCT_1:def 7;
then A18: h . x in P by A17, FUNCT_4:13;
x in dom h by A12, A17, XBOOLE_0:def 3;
then x in h " P by A18, FUNCT_1:def 7;
hence x in (h " P) /\ ([#] T2) by A16, XBOOLE_0:def 4; :: thesis: verum
end;
A19: for x being set st x in [#] T1 holds
h . x = f . x
proof
let x be set ; :: thesis: ( x in [#] T1 implies h . x = f . x )
assume A20: x in [#] T1 ; :: thesis: h . x = f . x
A21: dom g = the carrier of T2 by FUNCT_2:def 1;
per cases ( x in [#] T2 or not x in [#] T2 ) ;
suppose A22: x in [#] T2 ; :: thesis: h . x = f . x
then x in ([#] T1) /\ ([#] T2) by A20, XBOOLE_0:def 4;
then A23: x in X by A2;
then A24: ( (f | X) . x = f . x & (g | X) . x = g . x ) by FUNCT_1:49;
( x in dom (f | X) & x in dom (g | X) ) by A11, A20, A21, A22, A23, RELAT_1:57;
then x in (dom (f | X)) /\ (dom (g | X)) by XBOOLE_0:def 4;
then (f | X) . x = (g | X) . x by A8, PARTFUN1:def 4;
hence h . x = f . x by A9, A22, A24, FUNCT_4:13; :: thesis: verum
end;
suppose not x in [#] T2 ; :: thesis: h . x = f . x
hence h . x = f . x by A9, FUNCT_4:11; :: thesis: verum
end;
end;
end;
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) ) )
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) )
proof
assume A25: x in (h " P) /\ ([#] T1) ; :: thesis: x in f " P
then x in h " P by XBOOLE_0:def 4;
then A26: h . x in P by FUNCT_1:def 7;
f . x = h . x by A19, A25;
hence x in f " P by A11, A25, A26, FUNCT_1:def 7; :: thesis: verum
end;
assume A27: x in f " P ; :: thesis: x in (h " P) /\ ([#] T1)
then x in dom f by FUNCT_1:def 7;
then A28: x in dom h by A12, XBOOLE_0:def 3;
f . x in P by A27, FUNCT_1:def 7;
then h . x in P by A19, A27;
then x in h " P by A28, FUNCT_1:def 7;
hence x in (h " P) /\ ([#] T1) by A27, XBOOLE_0:def 4; :: thesis: verum
end;
then A29: (h " P) /\ ([#] T1) = f " P by TARSKI:2;
assume A30: P is closed ; :: thesis: h " P is closed
then f " P is closed by A6;
then f " P is compact by A3, Th8;
then A31: P1 is compact by Th19;
g " P is closed by A7, A30;
then g " P is compact by A4, Th8;
then A32: P2 is compact by Th19;
h " P = (h " P) /\ (([#] T1) \/ ([#] T2)) by A11, A9, A12, RELAT_1:132, XBOOLE_1:28
.= ((h " P) /\ ([#] T1)) \/ ((h " P) /\ ([#] T2)) by XBOOLE_1:23 ;
then h " P = (f " P) \/ (g " P) by A29, A13, TARSKI:2;
hence h " P is closed by A5, A31, A32; :: thesis: verum
end;
hence f +* g is continuous Function of T,S by PRE_TOPC:def 6; :: thesis: verum