:: Continuity of Mappings over the Union of Subspaces
:: by Zbigniew Karno
::
:: Received May 22, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

registration
let X be non empty TopSpace;
let X1, X2 be non empty SubSpace of X;
cluster X1 union X2 -> TopSpace-like ;
coherence
X1 union X2 is TopSpace-like ;
end;

definition
let A, B be non empty set ;
let A1, A2 be non empty Subset of A;
let f1 be Function of A1,B;
let f2 be Function of A2,B;
assume A1: f1 | (A1 /\ A2) = f2 | (A1 /\ A2) ;
func f1 union f2 -> Function of (A1 \/ A2),B means :Def1: :: TMAP_1:def 1
( it | A1 = f1 & it | A2 = f2 );
existence
ex b1 being Function of (A1 \/ A2),B st
( b1 | A1 = f1 & b1 | A2 = f2 )
proof end;
uniqueness
for b1, b2 being Function of (A1 \/ A2),B st b1 | A1 = f1 & b1 | A2 = f2 & b2 | A1 = f1 & b2 | A2 = f2 holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines union TMAP_1:def 1 :
for A, B being non empty set
for A1, A2 being non empty Subset of A
for f1 being Function of A1,B
for f2 being Function of A2,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) holds
for b7 being Function of (A1 \/ A2),B holds
( b7 = f1 union f2 iff ( b7 | A1 = f1 & b7 | A2 = f2 ) );

theorem Th1: :: TMAP_1:1
for A, B being non empty set
for A1, A2 being non empty Subset of A st A1 misses A2 holds
for f1 being Function of A1,B
for f2 being Function of A2,B holds
( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 )
proof end;

theorem Th2: :: TMAP_1:2
for A, B being non empty set
for A1, A2 being non empty Subset of A
for g being Function of (A1 \/ A2),B
for g1 being Function of A1,B
for g2 being Function of A2,B st g | A1 = g1 & g | A2 = g2 holds
g = g1 union g2
proof end;

theorem :: TMAP_1:3
for A, B being non empty set
for A1, A2 being non empty Subset of A
for f1 being Function of A1,B
for f2 being Function of A2,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) holds
f1 union f2 = f2 union f1
proof end;

theorem :: TMAP_1:4
for A, B being non empty set
for A1, A2, A3, A12, A23 being non empty Subset of A st A12 = A1 \/ A2 & A23 = A2 \/ A3 holds
for f1 being Function of A1,B
for f2 being Function of A2,B
for f3 being Function of A3,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds
for f12 being Function of A12,B
for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds
f12 union f3 = f1 union f23
proof end;

theorem :: TMAP_1:5
for A, B being non empty set
for A1, A2 being non empty Subset of A
for f1 being Function of A1,B
for f2 being Function of A2,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) holds
( ( A1 is Subset of A2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies A1 is Subset of A2 ) & ( A2 is Subset of A1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies A2 is Subset of A1 ) )
proof end;

begin

theorem Th6: :: TMAP_1:6
for X being TopStruct
for X0 being SubSpace of X holds TopStruct(# the carrier of X0, the topology of X0 #) is strict SubSpace of X
proof end;

theorem Th7: :: TMAP_1:7
for X being TopStruct
for X1, X2 being TopSpace st X1 = TopStruct(# the carrier of X2, the topology of X2 #) holds
( X1 is SubSpace of X iff X2 is SubSpace of X )
proof end;

theorem Th8: :: TMAP_1:8
for X, X1, X2 being TopSpace st X2 = TopStruct(# the carrier of X1, the topology of X1 #) holds
( X1 is closed SubSpace of X iff X2 is closed SubSpace of X )
proof end;

theorem Th9: :: TMAP_1:9
for X, X1, X2 being TopSpace st X2 = TopStruct(# the carrier of X1, the topology of X1 #) holds
( X1 is open SubSpace of X iff X2 is open SubSpace of X )
proof end;

theorem Th10: :: TMAP_1:10
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 is SubSpace of X2 holds
for x1 being Point of X1 ex x2 being Point of X2 st x2 = x1
proof end;

theorem Th11: :: TMAP_1:11
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for x being Point of (X1 union X2) holds
( ex x1 being Point of X1 st x1 = x or ex x2 being Point of X2 st x2 = x )
proof end;

theorem Th12: :: TMAP_1:12
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
for x being Point of (X1 meet X2) holds
( ex x1 being Point of X1 st x1 = x & ex x2 being Point of X2 st x2 = x )
proof end;

theorem :: TMAP_1:13
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for x being Point of (X1 union X2)
for F1 being Subset of X1
for F2 being Subset of X2 st F1 is closed & x in F1 & F2 is closed & x in F2 holds
ex H being Subset of (X1 union X2) st
( H is closed & x in H & H c= F1 \/ F2 )
proof end;

theorem Th14: :: TMAP_1:14
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for x being Point of (X1 union X2)
for U1 being Subset of X1
for U2 being Subset of X2 st U1 is open & x in U1 & U2 is open & x in U2 holds
ex V being Subset of (X1 union X2) st
( V is open & x in V & V c= U1 \/ U2 )
proof end;

theorem Th15: :: TMAP_1:15
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for x being Point of (X1 union X2)
for x1 being Point of X1
for x2 being Point of X2 st x1 = x & x2 = x holds
for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex V being Subset of (X1 union X2) st
( V is open & x in V & V c= A1 \/ A2 )
proof end;

theorem Th16: :: TMAP_1:16
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for x being Point of (X1 union X2)
for x1 being Point of X1
for x2 being Point of X2 st x1 = x & x2 = x holds
for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex A being a_neighborhood of x st A c= A1 \/ A2
proof end;

theorem Th17: :: TMAP_1:17
for X being non empty TopSpace
for X0, X1 being non empty SubSpace of X st X0 is SubSpace of X1 holds
( X0 meets X1 & X1 meets X0 )
proof end;

theorem Th18: :: TMAP_1:18
for X being non empty TopSpace
for X0, X1, X2 being non empty SubSpace of X st X0 is SubSpace of X1 & ( X0 meets X2 or X2 meets X0 ) holds
( X1 meets X2 & X2 meets X1 )
proof end;

theorem Th19: :: TMAP_1:19
for X being non empty TopSpace
for X0, X1, X2 being non empty SubSpace of X st X0 is SubSpace of X1 & ( X1 misses X2 or X2 misses X1 ) holds
( X0 misses X2 & X2 misses X0 )
proof end;

theorem :: TMAP_1:20
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds X0 union X0 = TopStruct(# the carrier of X0, the topology of X0 #)
proof end;

theorem :: TMAP_1:21
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds X0 meet X0 = TopStruct(# the carrier of X0, the topology of X0 #)
proof end;

theorem Th22: :: TMAP_1:22
for X being non empty TopSpace
for Y1, X1, Y2, X2 being non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 holds
Y1 union Y2 is SubSpace of X1 union X2
proof end;

theorem :: TMAP_1:23
for X being non empty TopSpace
for Y1, Y2, X1, X2 being non empty SubSpace of X st Y1 meets Y2 & Y1 is SubSpace of X1 & Y2 is SubSpace of X2 holds
Y1 meet Y2 is SubSpace of X1 meet X2
proof end;

theorem Th24: :: TMAP_1:24
for X being non empty TopSpace
for X1, X0, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & X2 is SubSpace of X0 holds
X1 union X2 is SubSpace of X0
proof end;

theorem :: TMAP_1:25
for X being non empty TopSpace
for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 & X1 is SubSpace of X0 & X2 is SubSpace of X0 holds
X1 meet X2 is SubSpace of X0
proof end;

theorem Th26: :: TMAP_1:26
for X being non empty TopSpace
for X1, X0, X2 being non empty SubSpace of X holds
( ( ( X1 misses X0 or X0 misses X1 ) & ( X2 meets X0 or X0 meets X2 ) implies ( (X1 union X2) meet X0 = X2 meet X0 & X0 meet (X1 union X2) = X0 meet X2 ) ) & ( ( X1 meets X0 or X0 meets X1 ) & ( X2 misses X0 or X0 misses X2 ) implies ( (X1 union X2) meet X0 = X1 meet X0 & X0 meet (X1 union X2) = X0 meet X1 ) ) )
proof end;

theorem Th27: :: TMAP_1:27
for X being non empty TopSpace
for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 holds
( ( X1 is SubSpace of X0 implies X1 meet X2 is SubSpace of X0 meet X2 ) & ( X2 is SubSpace of X0 implies X1 meet X2 is SubSpace of X1 meet X0 ) )
proof end;

theorem Th28: :: TMAP_1:28
for X being non empty TopSpace
for X1, X0, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & ( X0 misses X2 or X2 misses X0 ) holds
( X0 meet (X1 union X2) = TopStruct(# the carrier of X1, the topology of X1 #) & X0 meet (X2 union X1) = TopStruct(# the carrier of X1, the topology of X1 #) )
proof end;

theorem Th29: :: TMAP_1:29
for X being non empty TopSpace
for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 holds
( ( X1 is SubSpace of X0 implies ( X0 meet X2 meets X1 & X2 meet X0 meets X1 ) ) & ( X2 is SubSpace of X0 implies ( X1 meet X0 meets X2 & X0 meet X1 meets X2 ) ) )
proof end;

theorem Th30: :: TMAP_1:30
for X being non empty TopSpace
for X1, Y1, X2, Y2 being non empty SubSpace of X st X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & ( Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 ) holds
( Y1 misses X2 & Y2 misses X1 )
proof end;

theorem Th31: :: TMAP_1:31
for X being non empty TopSpace
for X1, X2, Y1, Y2 being non empty SubSpace of X st X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & X1 union X2 is SubSpace of Y1 union Y2 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 holds
( Y1 meets X1 union X2 & Y2 meets X1 union X2 )
proof end;

theorem Th32: :: TMAP_1:32
for X being non empty TopSpace
for X1, X2, Y1, Y2, X0 being non empty SubSpace of X st X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union X0 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & X0 meet (X1 union X2) is SubSpace of X1 meet X2 holds
( Y1 meets X1 union X2 & Y2 meets X1 union X2 )
proof end;

theorem Th33: :: TMAP_1:33
for X being non empty TopSpace
for X1, X2, Y1, Y2, X0 being non empty SubSpace of X st X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & X1 union X2 is not SubSpace of Y1 union Y2 & TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union X0 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & X0 meet (X1 union X2) is SubSpace of X1 meet X2 holds
( Y1 union Y2 meets X1 union X2 & X0 meets X1 union X2 )
proof end;

theorem Th34: :: TMAP_1:34
for X being non empty TopSpace
for X1, X2, X0 being non empty SubSpace of X holds
( ( not X1 union X2 meets X0 or X1 meets X0 or X2 meets X0 ) & ( ( X1 meets X0 or X2 meets X0 ) implies X1 union X2 meets X0 ) & ( not X0 meets X1 union X2 or X0 meets X1 or X0 meets X2 ) & ( ( X0 meets X1 or X0 meets X2 ) implies X0 meets X1 union X2 ) )
proof end;

theorem :: TMAP_1:35
for X being non empty TopSpace
for X1, X2, X0 being non empty SubSpace of X holds
( ( X1 union X2 misses X0 implies ( X1 misses X0 & X2 misses X0 ) ) & ( X1 misses X0 & X2 misses X0 implies X1 union X2 misses X0 ) & ( X0 misses X1 union X2 implies ( X0 misses X1 & X0 misses X2 ) ) & ( X0 misses X1 & X0 misses X2 implies X0 misses X1 union X2 ) )
proof end;

theorem :: TMAP_1:36
for X being non empty TopSpace
for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 holds
( ( X1 meet X2 meets X0 implies ( X1 meets X0 & X2 meets X0 ) ) & ( X0 meets X1 meet X2 implies ( X0 meets X1 & X0 meets X2 ) ) )
proof end;

theorem :: TMAP_1:37
for X being non empty TopSpace
for X1, X2, X0 being non empty SubSpace of X st X1 meets X2 holds
( ( ( X1 misses X0 or X2 misses X0 ) implies X1 meet X2 misses X0 ) & ( ( X0 misses X1 or X0 misses X2 ) implies X0 misses X1 meet X2 ) )
proof end;

theorem Th38: :: TMAP_1:38
for X being non empty TopSpace
for X1 being non empty SubSpace of X
for X0 being non empty closed SubSpace of X st X0 meets X1 holds
X0 meet X1 is closed SubSpace of X1
proof end;

theorem Th39: :: TMAP_1:39
for X being non empty TopSpace
for X1 being non empty SubSpace of X
for X0 being non empty open SubSpace of X st X0 meets X1 holds
X0 meet X1 is open SubSpace of X1
proof end;

theorem :: TMAP_1:40
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for X0 being non empty closed SubSpace of X st X1 is SubSpace of X0 & X0 misses X2 holds
( X1 is closed SubSpace of X1 union X2 & X1 is closed SubSpace of X2 union X1 )
proof end;

theorem Th41: :: TMAP_1:41
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for X0 being non empty open SubSpace of X st X1 is SubSpace of X0 & X0 misses X2 holds
( X1 is open SubSpace of X1 union X2 & X1 is open SubSpace of X2 union X1 )
proof end;

begin

definition
let X, Y be non empty TopSpace;
let f be Function of X,Y;
let x be Point of X;
pred f is_continuous_at x means :Def2: :: TMAP_1:def 2
 for G being a_neighborhood of f . x ex H being a_neighborhood of x st f .: H c= G;
end;

:: deftheorem Def2 defines is_continuous_at TMAP_1:def 2 :
for X, Y being non empty TopSpace
for f being Function of X,Y
for x being Point of X holds
( f is_continuous_at x iff for G being a_neighborhood of f . x ex H being a_neighborhood of x st f .: H c= G );

notation
let X, Y be non empty TopSpace;
let f be Function of X,Y;
let x be Point of X;
antonym f is_not_continuous_at x for f is_continuous_at x;
end;

theorem Th42: :: TMAP_1:42
for Y, X being non empty TopSpace
for f being Function of X,Y
for x being Point of X holds
( f is_continuous_at x iff for G being a_neighborhood of f . x holds f " G is a_neighborhood of x )
proof end;

theorem Th43: :: TMAP_1:43
for X, Y being non empty TopSpace
for f being Function of X,Y
for x being Point of X holds
( f is_continuous_at x iff for G being Subset of Y st G is open & f . x in G holds
ex H being Subset of X st
( H is open & x in H & f .: H c= G ) )
proof end;

theorem Th44: :: TMAP_1:44
for Y, X being non empty TopSpace
for f being Function of X,Y holds
( f is continuous iff for x being Point of X holds f is_continuous_at x )
proof end;

theorem Th45: :: TMAP_1:45
for X, Y, Z being non empty TopSpace st the carrier of Y = the carrier of Z & the topology of Z c= the topology of Y holds
for f being Function of X,Y
for g being Function of X,Z st f = g holds
for x being Point of X st f is_continuous_at x holds
g is_continuous_at x
proof end;

theorem Th46: :: TMAP_1:46
for X, Y, Z being non empty TopSpace st the carrier of X = the carrier of Y & the topology of Y c= the topology of X holds
for f being Function of X,Z
for g being Function of Y,Z st f = g holds
for x being Point of X
for y being Point of Y st x = y & g is_continuous_at y holds
f is_continuous_at x
proof end;

theorem Th47: :: TMAP_1:47
for Z, X, Y being non empty TopSpace
for f being Function of X,Y
for g being Function of Y,Z
for x being Point of X
for y being Point of Y st y = f . x & f is_continuous_at x & g is_continuous_at y holds
g * f is_continuous_at x
proof end;

theorem :: TMAP_1:48
for Z, Y, X being non empty TopSpace
for f being Function of X,Y
for g being Function of Y,Z
for y being Point of Y st f is continuous & g is_continuous_at y holds
for x being Point of X st x in f " {y} holds
g * f is_continuous_at x
proof end;

theorem :: TMAP_1:49
for Y, Z, X being non empty TopSpace
for f being Function of X,Y
for g being Function of Y,Z
for x being Point of X st f is_continuous_at x & g is continuous holds
g * f is_continuous_at x
proof end;

theorem :: TMAP_1:50
for X, Y being non empty TopSpace
for f being Function of X,Y holds
( f is continuous Function of X,Y iff for x being Point of X holds f is_continuous_at x ) by Th44;

theorem Th51: :: TMAP_1:51
for X, Y, Z being non empty TopSpace st the carrier of Y = the carrier of Z & the topology of Z c= the topology of Y holds
for f being continuous Function of X,Y holds f is continuous Function of X,Z
proof end;

theorem :: TMAP_1:52
for X, Y, Z being non empty TopSpace st the carrier of X = the carrier of Y & the topology of Y c= the topology of X holds
for f being continuous Function of Y,Z holds f is continuous Function of X,Z
proof end;

Lm1: for A being set holds {} is Function of A,{}
proof end;

definition
let S, T be 1-sorted ;
let f be Function of S,T;
let R be 1-sorted ;
assume A1: the carrier of R c= the carrier of S ;
func f | R -> Function of R,T equals :Def3: :: TMAP_1:def 3
f | the carrier of R;
coherence
f | the carrier of R is Function of R,T
proof end;
end;

:: deftheorem Def3 defines | TMAP_1:def 3 :
for S, T being 1-sorted
for f being Function of S,T
for R being 1-sorted st the carrier of R c= the carrier of S holds
f | R = f | the carrier of R;

definition
let X, Y be non empty TopSpace;
let f be Function of X,Y;
let X0 be SubSpace of X;
redefine func f | X0 equals :: TMAP_1:def 4
f | the carrier of X0;
compatibility
for b1 being Function of X0,Y holds
( b1 = f | X0 iff b1 = f | the carrier of X0 )
proof end;
end;

:: deftheorem defines | TMAP_1:def 4 :
for X, Y being non empty TopSpace
for f being Function of X,Y
for X0 being SubSpace of X holds f | X0 = f | the carrier of X0;

theorem Th53: :: TMAP_1:53
for Y, X being non empty TopSpace
for X0 being non empty SubSpace of X
for f being Function of X,Y
for f0 being Function of X0,Y st ( for x being Point of X st x in the carrier of X0 holds
f . x = f0 . x ) holds
f | X0 = f0
proof end;

theorem Th54: :: TMAP_1:54
for Y, X being non empty TopSpace
for X0 being non empty SubSpace of X
for f being Function of X,Y st TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of X, the topology of X #) holds
f = f | X0
proof end;

theorem :: TMAP_1:55
for Y, X being non empty TopSpace
for X0 being non empty SubSpace of X
for f being Function of X,Y
for A being Subset of X st A c= the carrier of X0 holds
f .: A = (f | X0) .: A by FUNCT_2:97;

theorem :: TMAP_1:56
for X, Y being non empty TopSpace
for X0 being non empty SubSpace of X
for f being Function of X,Y
for B being Subset of Y st f " B c= the carrier of X0 holds
f " B = (f | X0) " B by FUNCT_2:98;

theorem Th57: :: TMAP_1:57
for Y, X being non empty TopSpace
for X0 being non empty SubSpace of X
for g being Function of X0,Y ex h being Function of X,Y st h | X0 = g
proof end;

theorem Th58: :: TMAP_1:58
for Y, X being non empty TopSpace
for f being Function of X,Y
for X0 being non empty SubSpace of X
for x being Point of X
for x0 being Point of X0 st x = x0 & f is_continuous_at x holds
f | X0 is_continuous_at x0
proof end;

::Characterizations of Continuity at the Point by Local one.
theorem Th59: :: TMAP_1:59
for Y, X being non empty TopSpace
for f being Function of X,Y
for X0 being non empty SubSpace of X
for A being Subset of X
for x being Point of X
for x0 being Point of X0 st A c= the carrier of X0 & A is a_neighborhood of x & x = x0 holds
( f is_continuous_at x iff f | X0 is_continuous_at x0 )
proof end;

theorem Th60: :: TMAP_1:60
for Y, X being non empty TopSpace
for f being Function of X,Y
for X0 being non empty SubSpace of X
for A being Subset of X
for x being Point of X
for x0 being Point of X0 st A is open & x in A & A c= the carrier of X0 & x = x0 holds
( f is_continuous_at x iff f | X0 is_continuous_at x0 )
proof end;

theorem :: TMAP_1:61
for Y, X being non empty TopSpace
for f being Function of X,Y
for X0 being non empty open SubSpace of X
for x being Point of X
for x0 being Point of X0 st x = x0 holds
( f is_continuous_at x iff f | X0 is_continuous_at x0 )
proof end;

registration
let X, Y be non empty TopSpace;
let f be continuous Function of X,Y;
let X0 be non empty SubSpace of X;
cluster f | X0 -> continuous ;
coherence
f | X0 is continuous
proof end;
end;

theorem Th62: :: TMAP_1:62
for X, Y, Z being non empty TopSpace
for X0 being non empty SubSpace of X
for f being Function of X,Y
for g being Function of Y,Z holds (g * f) | X0 = g * (f | X0)
proof end;

theorem Th63: :: TMAP_1:63
for X, Y, Z being non empty TopSpace
for X0 being non empty SubSpace of X
for g being Function of Y,Z
for f being Function of X,Y st g is continuous & f | X0 is continuous holds
(g * f) | X0 is continuous
proof end;

theorem :: TMAP_1:64
for X, Y, Z being non empty TopSpace
for X0 being non empty SubSpace of X
for g being continuous Function of Y,Z
for f being Function of X,Y st f | X0 is continuous Function of X0,Y holds
(g * f) | X0 is continuous Function of X0,Z by Th63;

::(Definition of the restriction mapping - special case.)
definition
let X, Y be non empty TopSpace;
let X0, X1 be SubSpace of X;
let g be Function of X0,Y;
assume A1: X1 is SubSpace of X0 ;
func g | X1 -> Function of X1,Y equals :Def5: :: TMAP_1:def 5
g | the carrier of X1;
coherence
g | the carrier of X1 is Function of X1,Y
proof end;
end;

:: deftheorem Def5 defines | TMAP_1:def 5 :
for X, Y being non empty TopSpace
for X0, X1 being SubSpace of X
for g being Function of X0,Y st X1 is SubSpace of X0 holds
g | X1 = g | the carrier of X1;

theorem Th65: :: TMAP_1:65
for X, Y being non empty TopSpace
for X1, X0 being non empty SubSpace of X
for g being Function of X0,Y st X1 is SubSpace of X0 holds
for x0 being Point of X0 st x0 in the carrier of X1 holds
g . x0 = (g | X1) . x0
proof end;

theorem :: TMAP_1:66
for X, Y being non empty TopSpace
for X1, X0 being non empty SubSpace of X
for g being Function of X0,Y st X1 is SubSpace of X0 holds
for g1 being Function of X1,Y st ( for x0 being Point of X0 st x0 in the carrier of X1 holds
g . x0 = g1 . x0 ) holds
g | X1 = g1
proof end;

theorem Th67: :: TMAP_1:67
for X, Y being non empty TopSpace
for X0 being non empty SubSpace of X
for g being Function of X0,Y holds g = g | X0
proof end;

theorem Th68: :: TMAP_1:68
for X, Y being non empty TopSpace
for X1, X0 being non empty SubSpace of X
for g being Function of X0,Y st X1 is SubSpace of X0 holds
for A being Subset of X0 st A c= the carrier of X1 holds
g .: A = (g | X1) .: A
proof end;

theorem :: TMAP_1:69
for X, Y being non empty TopSpace
for X1, X0 being non empty SubSpace of X
for g being Function of X0,Y st X1 is SubSpace of X0 holds
for B being Subset of Y st g " B c= the carrier of X1 holds
g " B = (g | X1) " B
proof end;

theorem Th70: :: TMAP_1:70
for X, Y being non empty TopSpace
for X0, X1 being non empty SubSpace of X
for f being Function of X,Y
for g being Function of X0,Y st g = f | X0 & X1 is SubSpace of X0 holds
g | X1 = f | X1
proof end;

theorem Th71: :: TMAP_1:71
for X, Y being non empty TopSpace
for X1, X0 being non empty SubSpace of X
for f being Function of X,Y st X1 is SubSpace of X0 holds
(f | X0) | X1 = f | X1
proof end;

theorem Th72: :: TMAP_1:72
for X, Y being non empty TopSpace
for X0, X1, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & X2 is SubSpace of X1 holds
for g being Function of X0,Y holds (g | X1) | X2 = g | X2
proof end;

theorem :: TMAP_1:73
for X, Y being non empty TopSpace
for X1, X0 being non empty SubSpace of X
for f being Function of X,Y
for f0 being Function of X1,Y
for g being Function of X0,Y st X0 = X & f = g holds
( g | X1 = f0 iff f | X1 = f0 ) by Def5;

theorem Th74: :: TMAP_1:74
for X, Y being non empty TopSpace
for X0, X1 being non empty SubSpace of X
for g being Function of X0,Y
for x0 being Point of X0
for x1 being Point of X1 st x0 = x1 & X1 is SubSpace of X0 & g is_continuous_at x0 holds
g | X1 is_continuous_at x1
proof end;

theorem Th75: :: TMAP_1:75
for X, Y being non empty TopSpace
for X1, X0 being non empty SubSpace of X
for f being Function of X,Y st X1 is SubSpace of X0 holds
for x0 being Point of X0
for x1 being Point of X1 st x0 = x1 & f | X0 is_continuous_at x0 holds
f | X1 is_continuous_at x1
proof end;

::Characterizations of Continuity at the Point by Local one.
theorem Th76: :: TMAP_1:76
for X, Y being non empty TopSpace
for X1, X0 being non empty SubSpace of X
for g being Function of X0,Y st X1 is SubSpace of X0 holds
for A being Subset of X0
for x0 being Point of X0
for x1 being Point of X1 st A c= the carrier of X1 & A is a_neighborhood of x0 & x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
proof end;

theorem Th77: :: TMAP_1:77
for X, Y being non empty TopSpace
for X1, X0 being non empty SubSpace of X
for g being Function of X0,Y st X1 is SubSpace of X0 holds
for A being Subset of X0
for x0 being Point of X0
for x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 & x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
proof end;

theorem :: TMAP_1:78
for Y, X being non empty TopSpace
for X1, X0 being non empty SubSpace of X
for g being Function of X0,Y st X1 is SubSpace of X0 holds
for A being Subset of X
for x0 being Point of X0
for x1 being Point of X1 st A is open & x0 in A & A c= the carrier of X1 & x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
proof end;

theorem Th79: :: TMAP_1:79
for X, Y being non empty TopSpace
for X1, X0 being non empty SubSpace of X
for g being Function of X0,Y st X1 is open SubSpace of X0 holds
for x0 being Point of X0
for x1 being Point of X1 st x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
proof end;

theorem :: TMAP_1:80
for Y, X being non empty TopSpace
for X1, X0 being non empty SubSpace of X
for g being Function of X0,Y st X1 is open SubSpace of X & X1 is SubSpace of X0 holds
for x0 being Point of X0
for x1 being Point of X1 st x0 = x1 holds
( g is_continuous_at x0 iff g | X1 is_continuous_at x1 )
proof end;

theorem Th81: :: TMAP_1:81
for X, Y being non empty TopSpace
for X1, X0 being non empty SubSpace of X
for g being Function of X0,Y st TopStruct(# the carrier of X1, the topology of X1 #) = X0 holds
for x0 being Point of X0
for x1 being Point of X1 st x0 = x1 & g | X1 is_continuous_at x1 holds
g is_continuous_at x0
proof end;

theorem Th82: :: TMAP_1:82
for X, Y being non empty TopSpace
for X0, X1 being non empty SubSpace of X
for g being continuous Function of X0,Y st X1 is SubSpace of X0 holds
g | X1 is continuous Function of X1,Y
proof end;

theorem Th83: :: TMAP_1:83
for X, Y being non empty TopSpace
for X1, X0, X2 being non empty SubSpace of X st X1 is SubSpace of X0 & X2 is SubSpace of X1 holds
for g being Function of X0,Y st g | X1 is continuous Function of X1,Y holds
g | X2 is continuous Function of X2,Y
proof end;

registration
let X be non empty TopSpace;
cluster id X -> continuous ;
coherence
id X is continuous
proof end;
end;

::(Definition of the inclusion mapping.)
definition
let X be non empty TopSpace;
let X0 be SubSpace of X;
func incl X0 -> Function of X0,X equals :: TMAP_1:def 6
(id X) | X0;
coherence
(id X) | X0 is Function of X0,X ;
correctness
;
end;

:: deftheorem defines incl TMAP_1:def 6 :
for X being non empty TopSpace
for X0 being SubSpace of X holds incl X0 = (id X) | X0;

notation
let X be non empty TopSpace;
let X0 be SubSpace of X;
synonym X0 incl X for incl X0;
end;

theorem :: TMAP_1:84
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for x being Point of X st x in the carrier of X0 holds
(incl X0) . x = x
proof end;

theorem :: TMAP_1:85
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for f0 being Function of X0,X st ( for x being Point of X st x in the carrier of X0 holds
x = f0 . x ) holds
incl X0 = f0
proof end;

theorem :: TMAP_1:86
for X, Y being non empty TopSpace
for X0 being non empty SubSpace of X
for f being Function of X,Y holds f | X0 = f * (incl X0)
proof end;

theorem :: TMAP_1:87
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds incl X0 is continuous Function of X0,X ;

begin

definition
let X be non empty TopSpace;
let A be Subset of X;
func A -extension_of_the_topology_of X -> Subset-Family of X equals :: TMAP_1:def 7
 { (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } ;
coherence
{ (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } is Subset-Family of X
proof end;
end;

:: deftheorem defines -extension_of_the_topology_of TMAP_1:def 7 :
for X being non empty TopSpace
for A being Subset of X holds A -extension_of_the_topology_of X = { (H \/ (G /\ A)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } ;

theorem Th88: :: TMAP_1:88
for X being non empty TopSpace
for A being Subset of X holds the topology of X c= A -extension_of_the_topology_of X
proof end;

theorem Th89: :: TMAP_1:89
for X being non empty TopSpace
for A being Subset of X holds { (G /\ A) where G is Subset of X : G in the topology of X } c= A -extension_of_the_topology_of X
proof end;

theorem Th90: :: TMAP_1:90
for X being non empty TopSpace
for A, C, D being Subset of X st C in the topology of X & D in { (G /\ A) where G is Subset of X : G in the topology of X } holds
( C \/ D in A -extension_of_the_topology_of X & C /\ D in A -extension_of_the_topology_of X )
proof end;

theorem Th91: :: TMAP_1:91
for X being non empty TopSpace
for A being Subset of X holds A in A -extension_of_the_topology_of X
proof end;

theorem Th92: :: TMAP_1:92
for X being non empty TopSpace
for A being Subset of X holds
( A in the topology of X iff the topology of X = A -extension_of_the_topology_of X )
proof end;

definition
let X be non empty TopSpace;
let A be Subset of X;
func X modified_with_respect_to A -> strict TopSpace equals :: TMAP_1:def 8
 TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #);
coherence
TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #) is strict TopSpace
proof end;
end;

:: deftheorem defines modified_with_respect_to TMAP_1:def 8 :
for X being non empty TopSpace
for A being Subset of X holds X modified_with_respect_to A = TopStruct(# the carrier of X,(A -extension_of_the_topology_of X) #);

registration
let X be non empty TopSpace;
let A be Subset of X;
cluster X modified_with_respect_to A -> non empty strict ;
coherence
not X modified_with_respect_to A is empty ;
end;

theorem :: TMAP_1:93
for X being non empty TopSpace
for A being Subset of X holds
( the carrier of (X modified_with_respect_to A) = the carrier of X & the topology of (X modified_with_respect_to A) = A -extension_of_the_topology_of X ) ;

theorem Th94: :: TMAP_1:94
for X being non empty TopSpace
for A being Subset of X
for B being Subset of (X modified_with_respect_to A) st B = A holds
B is open
proof end;

theorem Th95: :: TMAP_1:95
for X being non empty TopSpace
for A being Subset of X holds
( A is open iff TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to A )
proof end;

definition
let X be non empty TopSpace;
let A be Subset of X;
func modid (X,A) -> Function of X,(X modified_with_respect_to A) equals :: TMAP_1:def 9
 id the carrier of X;
coherence
id the carrier of X is Function of X,(X modified_with_respect_to A) ;
end;

:: deftheorem defines modid TMAP_1:def 9 :
for X being non empty TopSpace
for A being Subset of X holds modid (X,A) = id the carrier of X;

theorem Th96: :: TMAP_1:96
for X being non empty TopSpace
for A being Subset of X
for x being Point of X st not x in A holds
modid (X,A) is_continuous_at x
proof end;

theorem Th97: :: TMAP_1:97
for X being non empty TopSpace
for A being Subset of X
for X0 being non empty SubSpace of X st the carrier of X0 misses A holds
for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0
proof end;

theorem Th98: :: TMAP_1:98
for X being non empty TopSpace
for A being Subset of X
for X0 being non empty SubSpace of X st the carrier of X0 = A holds
for x0 being Point of X0 holds (modid (X,A)) | X0 is_continuous_at x0
proof end;

theorem Th99: :: TMAP_1:99
for X being non empty TopSpace
for A being Subset of X
for X0 being non empty SubSpace of X st the carrier of X0 misses A holds
(modid (X,A)) | X0 is continuous Function of X0,(X modified_with_respect_to A)
proof end;

theorem Th100: :: TMAP_1:100
for X being non empty TopSpace
for A being Subset of X
for X0 being non empty SubSpace of X st the carrier of X0 = A holds
(modid (X,A)) | X0 is continuous Function of X0,(X modified_with_respect_to A)
proof end;

theorem Th101: :: TMAP_1:101
for X being non empty TopSpace
for A being Subset of X holds
( A is open iff modid (X,A) is continuous Function of X,(X modified_with_respect_to A) )
proof end;

definition
let X be non empty TopSpace;
let X0 be SubSpace of X;
func X modified_with_respect_to X0 -> strict TopSpace means :Def10: :: TMAP_1:def 10
 for A being Subset of X st A = the carrier of X0 holds
it = X modified_with_respect_to A;
existence
ex b1 being strict TopSpace st
for A being Subset of X st A = the carrier of X0 holds
b1 = X modified_with_respect_to A
proof end;
uniqueness
for b1, b2 being strict TopSpace st ( for A being Subset of X st A = the carrier of X0 holds
b1 = X modified_with_respect_to A ) & ( for A being Subset of X st A = the carrier of X0 holds
b2 = X modified_with_respect_to A ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines modified_with_respect_to TMAP_1:def 10 :
for X being non empty TopSpace
for X0 being SubSpace of X
for b3 being strict TopSpace holds
( b3 = X modified_with_respect_to X0 iff for A being Subset of X st A = the carrier of X0 holds
b3 = X modified_with_respect_to A );

registration
let X be non empty TopSpace;
let X0 be SubSpace of X;
cluster X modified_with_respect_to X0 -> non empty strict ;
coherence
not X modified_with_respect_to X0 is empty
proof end;
end;

theorem Th102: :: TMAP_1:102
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds
( the carrier of (X modified_with_respect_to X0) = the carrier of X & ( for A being Subset of X st A = the carrier of X0 holds
the topology of (X modified_with_respect_to X0) = A -extension_of_the_topology_of X ) )
proof end;

theorem :: TMAP_1:103
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for Y0 being SubSpace of X modified_with_respect_to X0 st the carrier of Y0 = the carrier of X0 holds
Y0 is open SubSpace of X modified_with_respect_to X0
proof end;

theorem :: TMAP_1:104
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds
( X0 is open SubSpace of X iff TopStruct(# the carrier of X, the topology of X #) = X modified_with_respect_to X0 )
proof end;

definition
let X be non empty TopSpace;
let X0 be SubSpace of X;
func modid (X,X0) -> Function of X,(X modified_with_respect_to X0) means :Def11: :: TMAP_1:def 11
 for A being Subset of X st A = the carrier of X0 holds
it = modid (X,A);
existence
ex b1 being Function of X,(X modified_with_respect_to X0) st
for A being Subset of X st A = the carrier of X0 holds
b1 = modid (X,A)
proof end;
uniqueness
for b1, b2 being Function of X,(X modified_with_respect_to X0) st ( for A being Subset of X st A = the carrier of X0 holds
b1 = modid (X,A) ) & ( for A being Subset of X st A = the carrier of X0 holds
b2 = modid (X,A) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines modid TMAP_1:def 11 :
for X being non empty TopSpace
for X0 being SubSpace of X
for b3 being Function of X,(X modified_with_respect_to X0) holds
( b3 = modid (X,X0) iff for A being Subset of X st A = the carrier of X0 holds
b3 = modid (X,A) );

theorem :: TMAP_1:105
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds modid (X,X0) = id X
proof end;

theorem Th106: :: TMAP_1:106
for X being non empty TopSpace
for X0, X1 being non empty SubSpace of X st X0 misses X1 holds
for x1 being Point of X1 holds (modid (X,X0)) | X1 is_continuous_at x1
proof end;

theorem Th107: :: TMAP_1:107
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for x0 being Point of X0 holds (modid (X,X0)) | X0 is_continuous_at x0
proof end;

theorem :: TMAP_1:108
for X being non empty TopSpace
for X0, X1 being non empty SubSpace of X st X0 misses X1 holds
(modid (X,X0)) | X1 is continuous Function of X1,(X modified_with_respect_to X0)
proof end;

theorem :: TMAP_1:109
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds (modid (X,X0)) | X0 is continuous Function of X0,(X modified_with_respect_to X0)
proof end;

theorem :: TMAP_1:110
for X being non empty TopSpace
for X0 being SubSpace of X holds
( X0 is open SubSpace of X iff modid (X,X0) is continuous Function of X,(X modified_with_respect_to X0) )
proof end;

begin

::Continuity at the Point of Mappings over the Union of Subspaces.
theorem Th111: :: TMAP_1:111
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for g being Function of (X1 union X2),Y
for x1 being Point of X1
for x2 being Point of X2
for x being Point of (X1 union X2) st x = x1 & x = x2 holds
( g is_continuous_at x iff ( g | X1 is_continuous_at x1 & g | X2 is_continuous_at x2 ) )
proof end;

theorem :: TMAP_1:112
for X, Y being non empty TopSpace
for f being Function of X,Y
for X1, X2 being non empty SubSpace of X
for x being Point of (X1 union X2)
for x1 being Point of X1
for x2 being Point of X2 st x = x1 & x = x2 holds
( f | (X1 union X2) is_continuous_at x iff ( f | X1 is_continuous_at x1 & f | X2 is_continuous_at x2 ) )
proof end;

theorem :: TMAP_1:113
for X, Y being non empty TopSpace
for f being Function of X,Y
for X1, X2 being non empty SubSpace of X st X = X1 union X2 holds
for x being Point of X
for x1 being Point of X1
for x2 being Point of X2 st x = x1 & x = x2 holds
( f is_continuous_at x iff ( f | X1 is_continuous_at x1 & f | X2 is_continuous_at x2 ) )
proof end;

::Continuity of Mappings over the Union of Subspaces.
theorem Th114: :: TMAP_1:114
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 are_weakly_separated holds
for g being Function of (X1 union X2),Y holds
( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) )
proof end;

theorem Th115: :: TMAP_1:115
for X, Y being non empty TopSpace
for X1, X2 being non empty closed SubSpace of X
for g being Function of (X1 union X2),Y holds
( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) )
proof end;

theorem Th116: :: TMAP_1:116
for X, Y being non empty TopSpace
for X1, X2 being non empty open SubSpace of X
for g being Function of (X1 union X2),Y holds
( g is continuous Function of (X1 union X2),Y iff ( g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y ) )
proof end;

theorem Th117: :: TMAP_1:117
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1,X2 are_weakly_separated holds
for f being Function of X,Y holds
( f | (X1 union X2) is continuous Function of (X1 union X2),Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) )
proof end;

theorem :: TMAP_1:118
for X, Y being non empty TopSpace
for f being Function of X,Y
for X1, X2 being non empty closed SubSpace of X holds
( f | (X1 union X2) is continuous Function of (X1 union X2),Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) )
proof end;

theorem :: TMAP_1:119
for X, Y being non empty TopSpace
for f being Function of X,Y
for X1, X2 being non empty open SubSpace of X holds
( f | (X1 union X2) is continuous Function of (X1 union X2),Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) )
proof end;

theorem Th120: :: TMAP_1:120
for X, Y being non empty TopSpace
for f being Function of X,Y
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1,X2 are_weakly_separated holds
( f is continuous Function of X,Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) )
proof end;

theorem Th121: :: TMAP_1:121
for X, Y being non empty TopSpace
for f being Function of X,Y
for X1, X2 being non empty closed SubSpace of X st X = X1 union X2 holds
( f is continuous Function of X,Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) )
proof end;

theorem Th122: :: TMAP_1:122
for X, Y being non empty TopSpace
for f being Function of X,Y
for X1, X2 being non empty open SubSpace of X st X = X1 union X2 holds
( f is continuous Function of X,Y iff ( f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y ) )
proof end;

::Some Characterizations of Separated Subspaces of Topological Spaces.
theorem Th123: :: TMAP_1:123
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace
for g being Function of (X1 union X2),Y st g | X1 is continuous Function of X1,Y & g | X2 is continuous Function of X2,Y holds
g is continuous Function of (X1 union X2),Y ) ) )
proof end;

theorem Th124: :: TMAP_1:124
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace
for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds
f | (X1 union X2) is continuous Function of (X1 union X2),Y ) ) )
proof end;

theorem :: TMAP_1:125
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 holds
( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace
for f being Function of X,Y st f | X1 is continuous Function of X1,Y & f | X2 is continuous Function of X2,Y holds
f is continuous Function of X,Y ) ) )
proof end;

begin

definition
let X, Y be non empty TopSpace;
let X1, X2 be non empty SubSpace of X;
let f1 be Function of X1,Y;
let f2 be Function of X2,Y;
assume A1: ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) ;
func f1 union f2 -> Function of (X1 union X2),Y means :Def12: :: TMAP_1:def 12
( it | X1 = f1 & it | X2 = f2 );
existence
ex b1 being Function of (X1 union X2),Y st
( b1 | X1 = f1 & b1 | X2 = f2 )
proof end;
uniqueness
for b1, b2 being Function of (X1 union X2),Y st b1 | X1 = f1 & b1 | X2 = f2 & b2 | X1 = f1 & b2 | X2 = f2 holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines union TMAP_1:def 12 :
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
for b7 being Function of (X1 union X2),Y holds
( b7 = f1 union f2 iff ( b7 | X1 = f1 & b7 | X2 = f2 ) );

theorem Th126: :: TMAP_1:126
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for g being Function of (X1 union X2),Y holds g = (g | X1) union (g | X2)
proof end;

theorem :: TMAP_1:127
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 holds
for g being Function of X,Y holds g = (g | X1) union (g | X2)
proof end;

theorem Th128: :: TMAP_1:128
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
for f1 being Function of X1,Y
for f2 being Function of X2,Y holds
( ( (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 ) iff f1 | (X1 meet X2) = f2 | (X1 meet X2) )
proof end;

theorem :: TMAP_1:129
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y st f1 | (X1 meet X2) = f2 | (X1 meet X2) holds
( ( X1 is SubSpace of X2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies X1 is SubSpace of X2 ) & ( X2 is SubSpace of X1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies X2 is SubSpace of X1 ) )
proof end;

theorem :: TMAP_1:130
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) holds
f1 union f2 = f2 union f1
proof end;

theorem :: TMAP_1:131
for X, Y being non empty TopSpace
for X1, X2, X3 being non empty SubSpace of X
for f1 being Function of X1,Y
for f2 being Function of X2,Y
for f3 being Function of X3,Y st ( X1 misses X2 or f1 | (X1 meet X2) = f2 | (X1 meet X2) ) & ( X1 misses X3 or f1 | (X1 meet X3) = f3 | (X1 meet X3) ) & ( X2 misses X3 or f2 | (X2 meet X3) = f3 | (X2 meet X3) ) holds
(f1 union f2) union f3 = f1 union (f2 union f3)
proof end;

::Continuity of the Union of Continuous Mappings.
::(Theorems presented below are suitable also in the case X = X1 union X2.)
theorem :: TMAP_1:132
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y st f1 | (X1 meet X2) = f2 | (X1 meet X2) & X1,X2 are_weakly_separated holds
f1 union f2 is continuous Function of (X1 union X2),Y
proof end;

theorem Th133: :: TMAP_1:133
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X1 misses X2 holds
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y st X1,X2 are_weakly_separated holds
f1 union f2 is continuous Function of (X1 union X2),Y
proof end;

theorem :: TMAP_1:134
for X, Y being non empty TopSpace
for X1, X2 being non empty closed SubSpace of X st X1 meets X2 holds
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y st f1 | (X1 meet X2) = f2 | (X1 meet X2) holds
f1 union f2 is continuous Function of (X1 union X2),Y
proof end;

theorem :: TMAP_1:135
for X, Y being non empty TopSpace
for X1, X2 being non empty open SubSpace of X st X1 meets X2 holds
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y st f1 | (X1 meet X2) = f2 | (X1 meet X2) holds
f1 union f2 is continuous Function of (X1 union X2),Y
proof end;

theorem :: TMAP_1:136
for X, Y being non empty TopSpace
for X1, X2 being non empty closed SubSpace of X st X1 misses X2 holds
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y
proof end;

theorem :: TMAP_1:137
for X, Y being non empty TopSpace
for X1, X2 being non empty open SubSpace of X st X1 misses X2 holds
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y
proof end;

::A Characterization of Separated Subspaces by means of Continuity of the Union
::of Continuous continuous mappings defined on the Subspaces.
theorem :: TMAP_1:138
for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X holds
( X1,X2 are_separated iff ( X1 misses X2 & ( for Y being non empty TopSpace
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y holds f1 union f2 is continuous Function of (X1 union X2),Y ) ) )
proof end;

::Continuity of the Union of Continuous Mappings (a special case).
theorem :: TMAP_1:139
for X, Y being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 holds
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y st (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 & X1,X2 are_weakly_separated holds
f1 union f2 is continuous Function of X,Y
proof end;

theorem :: TMAP_1:140
for X, Y being non empty TopSpace
for X1, X2 being non empty closed SubSpace of X
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y st X = X1 union X2 & (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 holds
f1 union f2 is continuous Function of X,Y
proof end;

theorem :: TMAP_1:141
for X, Y being non empty TopSpace
for X1, X2 being non empty open SubSpace of X
for f1 being continuous Function of X1,Y
for f2 being continuous Function of X2,Y st X = X1 union X2 & (f1 union f2) | X1 = f1 & (f1 union f2) | X2 = f2 holds
f1 union f2 is continuous Function of X,Y
proof end;