:: TMAP_1 semantic presentation

registration
let c1 be non empty TopSpace;
let c2, c3 be non empty SubSpace of c1;
cluster a2 union a3 -> TopSpace-like ;
coherence
c2 union c3 is TopSpace-like ;
end;

theorem Th1: :: TMAP_1:1
for b1, b2 being non empty set
for b3 being Function of b1,b2
for b4 being Subset of b1
for b5 being Subset of b2 holds
( b3 .: b4 c= b5 iff b4 c= b3 " b5 )
proof end;

theorem Th2: :: TMAP_1:2
for b1, b2 being non empty set
for b3 being Function of b1,b2
for b4 being non empty Subset of b1
for b5 being Function of b4,b2 st ( for b6 being Element of b1 st b6 in b4 holds
b3 . b6 = b5 . b6 ) holds
b3 | b4 = b5
proof end;

theorem Th3: :: TMAP_1:3
canceled;

theorem Th4: :: TMAP_1:4
for b1 being Function
for b2, b3 being set st b3 c= b2 holds
b1 .: b3 = (b1 | b2) .: b3
proof end;

theorem Th5: :: TMAP_1:5
for b1 being Function
for b2, b3 being set st b1 " b3 c= b2 holds
b1 " b3 = (b1 | b2) " b3
proof end;

definition
let c1, c2 be non empty set ;
let c3, c4 be non empty Subset of c1;
let c5 be Function of c3,c2;
let c6 be Function of c4,c2;
assume E5: c5 | (c3 /\ c4) = c6 | (c3 /\ c4) ;
func c5 union c6 -> Function of a3 \/ a4,a2 means :Def1: :: TMAP_1:def 1
( a7 | a3 = a5 & a7 | a4 = a6 );
existence
ex b1 being Function of c3 \/ c4,c2 st
( b1 | c3 = c5 & b1 | c4 = c6 )
proof end;
uniqueness
for b1, b2 being Function of c3 \/ c4,c2 st b1 | c3 = c5 & b1 | c4 = c6 & b2 | c3 = c5 & b2 | c4 = c6 holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines union TMAP_1:def 1 :
for b1, b2 being non empty set
for b3, b4 being non empty Subset of b1
for b5 being Function of b3,b2
for b6 being Function of b4,b2 st b5 | (b3 /\ b4) = b6 | (b3 /\ b4) holds
for b7 being Function of b3 \/ b4,b2 holds
( b7 = b5 union b6 iff ( b7 | b3 = b5 & b7 | b4 = b6 ) );

theorem Th6: :: TMAP_1:6
for b1, b2 being non empty set
for b3, b4 being non empty Subset of b1 st b3 misses b4 holds
for b5 being Function of b3,b2
for b6 being Function of b4,b2 holds
( b5 | (b3 /\ b4) = b6 | (b3 /\ b4) & (b5 union b6) | b3 = b5 & (b5 union b6) | b4 = b6 )
proof end;

theorem Th7: :: TMAP_1:7
for b1, b2 being non empty set
for b3, b4 being non empty Subset of b1
for b5 being Function of b3 \/ b4,b2
for b6 being Function of b3,b2
for b7 being Function of b4,b2 st b5 | b3 = b6 & b5 | b4 = b7 holds
b5 = b6 union b7
proof end;

theorem Th8: :: TMAP_1:8
for b1, b2 being non empty set
for b3, b4 being non empty Subset of b1
for b5 being Function of b3,b2
for b6 being Function of b4,b2 st b5 | (b3 /\ b4) = b6 | (b3 /\ b4) holds
b5 union b6 = b6 union b5
proof end;

theorem Th9: :: TMAP_1:9
for b1, b2 being non empty set
for b3, b4, b5, b6, b7 being non empty Subset of b1 st b6 = b3 \/ b4 & b7 = b4 \/ b5 holds
for b8 being Function of b3,b2
for b9 being Function of b4,b2
for b10 being Function of b5,b2 st b8 | (b3 /\ b4) = b9 | (b3 /\ b4) & b9 | (b4 /\ b5) = b10 | (b4 /\ b5) & b8 | (b3 /\ b5) = b10 | (b3 /\ b5) holds
for b11 being Function of b6,b2
for b12 being Function of b7,b2 st b11 = b8 union b9 & b12 = b9 union b10 holds
b11 union b10 = b8 union b12
proof end;

theorem Th10: :: TMAP_1:10
for b1, b2 being non empty set
for b3, b4 being non empty Subset of b1
for b5 being Function of b3,b2
for b6 being Function of b4,b2 st b5 | (b3 /\ b4) = b6 | (b3 /\ b4) holds
( ( b3 is Subset of b4 implies b5 union b6 = b6 ) & ( b5 union b6 = b6 implies b3 is Subset of b4 ) & ( b4 is Subset of b3 implies b5 union b6 = b5 ) & ( b5 union b6 = b5 implies b4 is Subset of b3 ) )
proof end;

Lemma8: for b1 being TopSpace holds TopStruct(# the carrier of b1,the topology of b1 #) is TopSpace-like
proof end;

theorem Th11: :: TMAP_1:11
for b1 being TopStruct
for b2 being SubSpace of b1 holds TopStruct(# the carrier of b2,the topology of b2 #) is strict SubSpace of b1
proof end;

theorem Th12: :: TMAP_1:12
for b1 being TopStruct
for b2, b3 being TopSpace st b2 = TopStruct(# the carrier of b3,the topology of b3 #) holds
( b2 is SubSpace of b1 iff b3 is SubSpace of b1 )
proof end;

theorem Th13: :: TMAP_1:13
for b1, b2, b3 being TopSpace st b3 = TopStruct(# the carrier of b2,the topology of b2 #) holds
( b2 is closed SubSpace of b1 iff b3 is closed SubSpace of b1 )
proof end;

theorem Th14: :: TMAP_1:14
for b1, b2, b3 being TopSpace st b3 = TopStruct(# the carrier of b2,the topology of b2 #) holds
( b2 is open SubSpace of b1 iff b3 is open SubSpace of b1 )
proof end;

theorem Th15: :: TMAP_1:15
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1 st b2 is SubSpace of b3 holds
for b4 being Point of b2 ex b5 being Point of b3 st b5 = b4
proof end;

theorem Th16: :: TMAP_1:16
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1
for b4 being Point of (b2 union b3) holds
( ex b5 being Point of b2 st b5 = b4 or ex b5 being Point of b3 st b5 = b4 )
proof end;

theorem Th17: :: TMAP_1:17
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1 st b2 meets b3 holds
for b4 being Point of (b2 meet b3) holds
( ex b5 being Point of b2 st b5 = b4 & ex b5 being Point of b3 st b5 = b4 )
proof end;

theorem Th18: :: TMAP_1:18
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1
for b4 being Point of (b2 union b3)
for b5 being Subset of b2
for b6 being Subset of b3 st b5 is closed & b4 in b5 & b6 is closed & b4 in b6 holds
ex b7 being Subset of (b2 union b3) st
( b7 is closed & b4 in b7 & b7 c= b5 \/ b6 )
proof end;

theorem Th19: :: TMAP_1:19
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1
for b4 being Point of (b2 union b3)
for b5 being Subset of b2
for b6 being Subset of b3 st b5 is open & b4 in b5 & b6 is open & b4 in b6 holds
ex b7 being Subset of (b2 union b3) st
( b7 is open & b4 in b7 & b7 c= b5 \/ b6 )
proof end;

theorem Th20: :: TMAP_1:20
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1
for b4 being Point of (b2 union b3)
for b5 being Point of b2
for b6 being Point of b3 st b5 = b4 & b6 = b4 holds
for b7 being a_neighborhood of b5
for b8 being a_neighborhood of b6 ex b9 being Subset of (b2 union b3) st
( b9 is open & b4 in b9 & b9 c= b7 \/ b8 )
proof end;

theorem Th21: :: TMAP_1:21
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1
for b4 being Point of (b2 union b3)
for b5 being Point of b2
for b6 being Point of b3 st b5 = b4 & b6 = b4 holds
for b7 being a_neighborhood of b5
for b8 being a_neighborhood of b6 ex b9 being a_neighborhood of b4 st b9 c= b7 \/ b8
proof end;

theorem Th22: :: TMAP_1:22
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1 st b2 is SubSpace of b3 holds
( b2 meets b3 & b3 meets b2 )
proof end;

theorem Th23: :: TMAP_1:23
for b1 being non empty TopSpace
for b2, b3, b4 being non empty SubSpace of b1 st b2 is SubSpace of b3 & ( b2 meets b4 or b4 meets b2 ) holds
( b3 meets b4 & b4 meets b3 )
proof end;

theorem Th24: :: TMAP_1:24
for b1 being non empty TopSpace
for b2, b3, b4 being non empty SubSpace of b1 st b2 is SubSpace of b3 & ( b3 misses b4 or b4 misses b3 ) holds
( b2 misses b4 & b4 misses b2 )
proof end;

theorem Th25: :: TMAP_1:25
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1 holds b2 union b2 = TopStruct(# the carrier of b2,the topology of b2 #)
proof end;

theorem Th26: :: TMAP_1:26
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1 holds b2 meet b2 = TopStruct(# the carrier of b2,the topology of b2 #)
proof end;

theorem Th27: :: TMAP_1:27
for b1 being non empty TopSpace
for b2, b3, b4, b5 being non empty SubSpace of b1 st b2 is SubSpace of b3 & b4 is SubSpace of b5 holds
b2 union b4 is SubSpace of b3 union b5
proof end;

theorem Th28: :: TMAP_1:28
for b1 being non empty TopSpace
for b2, b3, b4, b5 being non empty SubSpace of b1 st b2 meets b3 & b2 is SubSpace of b4 & b3 is SubSpace of b5 holds
b2 meet b3 is SubSpace of b4 meet b5
proof end;

theorem Th29: :: TMAP_1:29
for b1 being non empty TopSpace
for b2, b3, b4 being non empty SubSpace of b1 st b2 is SubSpace of b3 & b4 is SubSpace of b3 holds
b2 union b4 is SubSpace of b3
proof end;

theorem Th30: :: TMAP_1:30
for b1 being non empty TopSpace
for b2, b3, b4 being non empty SubSpace of b1 st b2 meets b3 & b2 is SubSpace of b4 & b3 is SubSpace of b4 holds
b2 meet b3 is SubSpace of b4
proof end;

theorem Th31: :: TMAP_1:31
for b1 being non empty TopSpace
for b2, b3, b4 being non empty SubSpace of b1 holds
( ( ( b2 misses b3 or b3 misses b2 ) & ( b4 meets b3 or b3 meets b4 ) implies ( (b2 union b4) meet b3 = b4 meet b3 & b3 meet (b2 union b4) = b3 meet b4 ) ) & ( ( b2 meets b3 or b3 meets b2 ) & ( b4 misses b3 or b3 misses b4 ) implies ( (b2 union b4) meet b3 = b2 meet b3 & b3 meet (b2 union b4) = b3 meet b2 ) ) )
proof end;

theorem Th32: :: TMAP_1:32
for b1 being non empty TopSpace
for b2, b3, b4 being non empty SubSpace of b1 st b2 meets b3 holds
( ( b2 is SubSpace of b4 implies b2 meet b3 is SubSpace of b4 meet b3 ) & ( b3 is SubSpace of b4 implies b2 meet b3 is SubSpace of b2 meet b4 ) )
proof end;

theorem Th33: :: TMAP_1:33
for b1 being non empty TopSpace
for b2, b3, b4 being non empty SubSpace of b1 st b2 is SubSpace of b3 & ( b3 misses b4 or b4 misses b3 ) holds
( b3 meet (b2 union b4) = TopStruct(# the carrier of b2,the topology of b2 #) & b3 meet (b4 union b2) = TopStruct(# the carrier of b2,the topology of b2 #) )
proof end;

theorem Th34: :: TMAP_1:34
for b1 being non empty TopSpace
for b2, b3, b4 being non empty SubSpace of b1 st b2 meets b3 holds
( ( b2 is SubSpace of b4 implies ( b4 meet b3 meets b2 & b3 meet b4 meets b2 ) ) & ( b3 is SubSpace of b4 implies ( b2 meet b4 meets b3 & b4 meet b2 meets b3 ) ) )
proof end;

theorem Th35: :: TMAP_1:35
for b1 being non empty TopSpace
for b2, b3, b4, b5 being non empty SubSpace of b1 st b2 is SubSpace of b3 & b4 is SubSpace of b5 & ( b3 misses b5 or b3 meet b5 misses b2 union b4 ) holds
( b3 misses b4 & b5 misses b2 )
proof end;

theorem Th36: :: TMAP_1:36
for b1 being non empty TopSpace
for b2, b3, b4, b5 being non empty SubSpace of b1 st b2 is not SubSpace of b3 & b3 is not SubSpace of b2 & b2 union b3 is SubSpace of b4 union b5 & b4 meet (b2 union b3) is SubSpace of b2 & b5 meet (b2 union b3) is SubSpace of b3 holds
( b4 meets b2 union b3 & b5 meets b2 union b3 )
proof end;

theorem Th37: :: TMAP_1:37
for b1 being non empty TopSpace
for b2, b3, b4, b5, b6 being non empty SubSpace of b1 st b2 meets b3 & b2 is not SubSpace of b3 & b3 is not SubSpace of b2 & TopStruct(# the carrier of b1,the topology of b1 #) = (b4 union b5) union b6 & b4 meet (b2 union b3) is SubSpace of b2 & b5 meet (b2 union b3) is SubSpace of b3 & b6 meet (b2 union b3) is SubSpace of b2 meet b3 holds
( b4 meets b2 union b3 & b5 meets b2 union b3 )
proof end;

theorem Th38: :: TMAP_1:38
for b1 being non empty TopSpace
for b2, b3, b4, b5, b6 being non empty SubSpace of b1 st b2 meets b3 & b2 is not SubSpace of b3 & b3 is not SubSpace of b2 & b2 union b3 is not SubSpace of b4 union b5 & TopStruct(# the carrier of b1,the topology of b1 #) = (b4 union b5) union b6 & b4 meet (b2 union b3) is SubSpace of b2 & b5 meet (b2 union b3) is SubSpace of b3 & b6 meet (b2 union b3) is SubSpace of b2 meet b3 holds
( b4 union b5 meets b2 union b3 & b6 meets b2 union b3 )
proof end;

theorem Th39: :: TMAP_1:39
for b1 being non empty TopSpace
for b2, b3, b4 being non empty SubSpace of b1 holds
( ( not b2 union b3 meets b4 or b2 meets b4 or b3 meets b4 ) & ( ( b2 meets b4 or b3 meets b4 ) implies b2 union b3 meets b4 ) & ( not b4 meets b2 union b3 or b4 meets b2 or b4 meets b3 ) & ( ( b4 meets b2 or b4 meets b3 ) implies b4 meets b2 union b3 ) )
proof end;

theorem Th40: :: TMAP_1:40
for b1 being non empty TopSpace
for b2, b3, b4 being non empty SubSpace of b1 holds
( ( b2 union b3 misses b4 implies ( b2 misses b4 & b3 misses b4 ) ) & ( b2 misses b4 & b3 misses b4 implies b2 union b3 misses b4 ) & ( b4 misses b2 union b3 implies ( b4 misses b2 & b4 misses b3 ) ) & ( b4 misses b2 & b4 misses b3 implies b4 misses b2 union b3 ) )
proof end;

theorem Th41: :: TMAP_1:41
for b1 being non empty TopSpace
for b2, b3, b4 being non empty SubSpace of b1 st b2 meets b3 holds
( ( b2 meet b3 meets b4 implies ( b2 meets b4 & b3 meets b4 ) ) & ( b4 meets b2 meet b3 implies ( b4 meets b2 & b4 meets b3 ) ) )
proof end;

theorem Th42: :: TMAP_1:42
for b1 being non empty TopSpace
for b2, b3, b4 being non empty SubSpace of b1 st b2 meets b3 holds
( ( ( b2 misses b4 or b3 misses b4 ) implies b2 meet b3 misses b4 ) & ( ( b4 misses b2 or b4 misses b3 ) implies b4 misses b2 meet b3 ) )
proof end;

theorem Th43: :: TMAP_1:43
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1
for b3 being non empty closed SubSpace of b1 st b3 meets b2 holds
b3 meet b2 is closed SubSpace of b2
proof end;

theorem Th44: :: TMAP_1:44
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1
for b3 being non empty open SubSpace of b1 st b3 meets b2 holds
b3 meet b2 is open SubSpace of b2
proof end;

theorem Th45: :: TMAP_1:45
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1
for b4 being non empty closed SubSpace of b1 st b2 is SubSpace of b4 & b4 misses b3 holds
( b2 is closed SubSpace of b2 union b3 & b2 is closed SubSpace of b3 union b2 )
proof end;

theorem Th46: :: TMAP_1:46
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1
for b4 being non empty open SubSpace of b1 st b2 is SubSpace of b4 & b4 misses b3 holds
( b2 is open SubSpace of b2 union b3 & b2 is open SubSpace of b3 union b2 )
proof end;

definition
let c1, c2 be non empty TopSpace;
let c3 be Function of c1,c2;
let c4 be Point of c1;
pred c3 is_continuous_at c4 means :Def2: :: TMAP_1:def 2
for b1 being a_neighborhood of a3 . a4 ex b2 being a_neighborhood of a4 st a3 .: b2 c= b1;
end;

:: deftheorem Def2 defines is_continuous_at TMAP_1:def 2 :
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2
for b4 being Point of b1 holds
( b3 is_continuous_at b4 iff for b5 being a_neighborhood of b3 . b4 ex b6 being a_neighborhood of b4 st b3 .: b6 c= b5 );

notation
let c1, c2 be non empty TopSpace;
let c3 be Function of c1,c2;
let c4 be Point of c1;
antonym c3 is_not_continuous_at c4 for c3 is_continuous_at c4;
end;

theorem Th47: :: TMAP_1:47
for b1, b2 being non empty TopSpace
for b3 being Function of b2,b1
for b4 being Point of b2 holds
( b3 is_continuous_at b4 iff for b5 being a_neighborhood of b3 . b4 holds b3 " b5 is a_neighborhood of b4 )
proof end;

theorem Th48: :: TMAP_1:48
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2
for b4 being Point of b1 holds
( b3 is_continuous_at b4 iff for b5 being Subset of b2 st b5 is open & b3 . b4 in b5 holds
ex b6 being Subset of b1 st
( b6 is open & b4 in b6 & b3 .: b6 c= b5 ) )
proof end;

theorem Th49: :: TMAP_1:49
for b1, b2 being non empty TopSpace
for b3 being Function of b2,b1 holds
( b3 is continuous iff for b4 being Point of b2 holds b3 is_continuous_at b4 )
proof end;

theorem Th50: :: TMAP_1:50
for b1, b2, b3 being non empty TopSpace st the carrier of b2 = the carrier of b3 & the topology of b3 c= the topology of b2 holds
for b4 being Function of b1,b2
for b5 being Function of b1,b3 st b4 = b5 holds
for b6 being Point of b1 st b4 is_continuous_at b6 holds
b5 is_continuous_at b6
proof end;

theorem Th51: :: TMAP_1:51
for b1, b2, b3 being non empty TopSpace st the carrier of b1 = the carrier of b2 & the topology of b2 c= the topology of b1 holds
for b4 being Function of b1,b3
for b5 being Function of b2,b3 st b4 = b5 holds
for b6 being Point of b1
for b7 being Point of b2 st b6 = b7 & b5 is_continuous_at b7 holds
b4 is_continuous_at b6
proof end;

theorem Th52: :: TMAP_1:52
for b1, b2, b3 being non empty TopSpace
for b4 being Function of b2,b3
for b5 being Function of b3,b1
for b6 being Point of b2
for b7 being Point of b3 st b7 = b4 . b6 & b4 is_continuous_at b6 & b5 is_continuous_at b7 holds
b5 * b4 is_continuous_at b6
proof end;

theorem Th53: :: TMAP_1:53
for b1, b2, b3 being non empty TopSpace
for b4 being Function of b3,b2
for b5 being Function of b2,b1
for b6 being Point of b2 st b4 is continuous & b5 is_continuous_at b6 holds
for b7 being Point of b3 st b7 in b4 " {b6} holds
b5 * b4 is_continuous_at b7
proof end;

theorem Th54: :: TMAP_1:54
for b1, b2, b3 being non empty TopSpace
for b4 being Function of b3,b1
for b5 being Function of b1,b2
for b6 being Point of b3 st b4 is_continuous_at b6 & b5 is continuous holds
b5 * b4 is_continuous_at b6
proof end;

theorem Th55: :: TMAP_1:55
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2 holds
( b3 is continuous Function of b1,b2 iff for b4 being Point of b1 holds b3 is_continuous_at b4 ) by Th49;

theorem Th56: :: TMAP_1:56
for b1, b2, b3 being non empty TopSpace st the carrier of b2 = the carrier of b3 & the topology of b3 c= the topology of b2 holds
for b4 being continuous Function of b1,b2 holds b4 is continuous Function of b1,b3
proof end;

theorem Th57: :: TMAP_1:57
for b1, b2, b3 being non empty TopSpace st the carrier of b1 = the carrier of b2 & the topology of b2 c= the topology of b1 holds
for b4 being continuous Function of b2,b3 holds b4 is continuous Function of b1,b3
proof end;

definition
let c1, c2 be non empty TopSpace;
let c3 be SubSpace of c1;
let c4 be Function of c1,c2;
func c4 | c3 -> Function of a3,a2 equals :: TMAP_1:def 3
a4 | the carrier of a3;
coherence
c4 | the carrier of c3 is Function of c3,c2
proof end;
end;

:: deftheorem Def3 defines | TMAP_1:def 3 :
for b1, b2 being non empty TopSpace
for b3 being SubSpace of b1
for b4 being Function of b1,b2 holds b4 | b3 = b4 | the carrier of b3;

theorem Th58: :: TMAP_1:58
for b1, b2 being non empty TopSpace
for b3 being non empty SubSpace of b2
for b4 being Function of b2,b1
for b5 being Point of b2 st b5 in the carrier of b3 holds
b4 . b5 = (b4 | b3) . b5 by FUNCT_1:72;

theorem Th59: :: TMAP_1:59
for b1, b2 being non empty TopSpace
for b3 being non empty SubSpace of b2
for b4 being Function of b2,b1
for b5 being Function of b3,b1 st ( for b6 being Point of b2 st b6 in the carrier of b3 holds
b4 . b6 = b5 . b6 ) holds
b4 | b3 = b5
proof end;

theorem Th60: :: TMAP_1:60
for b1, b2 being non empty TopSpace
for b3 being non empty SubSpace of b2
for b4 being Function of b2,b1 st TopStruct(# the carrier of b3,the topology of b3 #) = TopStruct(# the carrier of b2,the topology of b2 #) holds
b4 = b4 | b3
proof end;

theorem Th61: :: TMAP_1:61
for b1, b2 being non empty TopSpace
for b3 being non empty SubSpace of b2
for b4 being Function of b2,b1
for b5 being Subset of b2 st b5 c= the carrier of b3 holds
b4 .: b5 = (b4 | b3) .: b5 by Th4;

theorem Th62: :: TMAP_1:62
for b1, b2 being non empty TopSpace
for b3 being non empty SubSpace of b1
for b4 being Function of b1,b2
for b5 being Subset of b2 st b4 " b5 c= the carrier of b3 holds
b4 " b5 = (b4 | b3) " b5 by Th5;

theorem Th63: :: TMAP_1:63
for b1, b2 being non empty TopSpace
for b3 being non empty SubSpace of b2
for b4 being Function of b3,b1 ex b5 being Function of b2,b1 st b5 | b3 = b4
proof end;

theorem Th64: :: TMAP_1:64
for b1, b2 being non empty TopSpace
for b3 being Function of b2,b1
for b4 being non empty SubSpace of b2
for b5 being Point of b2
for b6 being Point of b4 st b5 = b6 & b3 is_continuous_at b5 holds
b3 | b4 is_continuous_at b6
proof end;

theorem Th65: :: TMAP_1:65
for b1, b2 being non empty TopSpace
for b3 being Function of b2,b1
for b4 being non empty SubSpace of b2
for b5 being Subset of b2
for b6 being Point of b2
for b7 being Point of b4 st b5 c= the carrier of b4 & b5 is a_neighborhood of b6 & b6 = b7 holds
( b3 is_continuous_at b6 iff b3 | b4 is_continuous_at b7 )
proof end;

theorem Th66: :: TMAP_1:66
for b1, b2 being non empty TopSpace
for b3 being Function of b2,b1
for b4 being non empty SubSpace of b2
for b5 being Subset of b2
for b6 being Point of b2
for b7 being Point of b4 st b5 is open & b6 in b5 & b5 c= the carrier of b4 & b6 = b7 holds
( b3 is_continuous_at b6 iff b3 | b4 is_continuous_at b7 )
proof end;

theorem Th67: :: TMAP_1:67
for b1, b2 being non empty TopSpace
for b3 being Function of b2,b1
for b4 being non empty open SubSpace of b2
for b5 being Point of b2
for b6 being Point of b4 st b5 = b6 holds
( b3 is_continuous_at b5 iff b3 | b4 is_continuous_at b6 )
proof end;

theorem Th68: :: TMAP_1:68
for b1, b2 being non empty TopSpace
for b3 being continuous Function of b1,b2
for b4 being non empty SubSpace of b1 holds b3 | b4 is continuous Function of b4,b2
proof end;

theorem Th69: :: TMAP_1:69
for b1, b2, b3 being non empty TopSpace
for b4 being non empty SubSpace of b1
for b5 being Function of b1,b2
for b6 being Function of b2,b3 holds (b6 * b5) | b4 = b6 * (b5 | b4)
proof end;

theorem Th70: :: TMAP_1:70
for b1, b2, b3 being non empty TopSpace
for b4 being non empty SubSpace of b1
for b5 being Function of b2,b3
for b6 being Function of b1,b2 st b5 is continuous & b6 | b4 is continuous holds
(b5 * b6) | b4 is continuous
proof end;

theorem Th71: :: TMAP_1:71
for b1, b2, b3 being non empty TopSpace
for b4 being non empty SubSpace of b1
for b5 being continuous Function of b2,b3
for b6 being Function of b1,b2 st b6 | b4 is continuous Function of b4,b2 holds
(b5 * b6) | b4 is continuous Function of b4,b3 by Th70;

definition
let c1, c2 be non empty TopSpace;
let c3, c4 be SubSpace of c1;
let c5 be Function of c3,c2;
assume E55: c4 is SubSpace of c3 ;
func c5 | c4 -> Function of a4,a2 equals :Def4: :: TMAP_1:def 4
a5 | the carrier of a4;
coherence
c5 | the carrier of c4 is Function of c4,c2
proof end;
end;

:: deftheorem Def4 defines | TMAP_1:def 4 :
for b1, b2 being non empty TopSpace
for b3, b4 being SubSpace of b1
for b5 being Function of b3,b2 st b4 is SubSpace of b3 holds
b5 | b4 = b5 | the carrier of b4;

theorem Th72: :: TMAP_1:72
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b4,b2 st b3 is SubSpace of b4 holds
for b6 being Point of b4 st b6 in the carrier of b3 holds
b5 . b6 = (b5 | b3) . b6
proof end;

theorem Th73: :: TMAP_1:73
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b4,b2 st b3 is SubSpace of b4 holds
for b6 being Function of b3,b2 st ( for b7 being Point of b4 st b7 in the carrier of b3 holds
b5 . b7 = b6 . b7 ) holds
b5 | b3 = b6
proof end;

theorem Th74: :: TMAP_1:74
for b1, b2 being non empty TopSpace
for b3 being non empty SubSpace of b1
for b4 being Function of b3,b2 holds b4 = b4 | b3
proof end;

theorem Th75: :: TMAP_1:75
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b4,b2 st b3 is SubSpace of b4 holds
for b6 being Subset of b4 st b6 c= the carrier of b3 holds
b5 .: b6 = (b5 | b3) .: b6
proof end;

theorem Th76: :: TMAP_1:76
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b4,b2 st b3 is SubSpace of b4 holds
for b6 being Subset of b2 st b5 " b6 c= the carrier of b3 holds
b5 " b6 = (b5 | b3) " b6
proof end;

theorem Th77: :: TMAP_1:77
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b1,b2
for b6 being Function of b3,b2 st b6 = b5 | b3 & b4 is SubSpace of b3 holds
b6 | b4 = b5 | b4
proof end;

theorem Th78: :: TMAP_1:78
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b1,b2 st b3 is SubSpace of b4 holds
(b5 | b4) | b3 = b5 | b3
proof end;

theorem Th79: :: TMAP_1:79
for b1, b2 being non empty TopSpace
for b3, b4, b5 being non empty SubSpace of b1 st b4 is SubSpace of b3 & b5 is SubSpace of b4 holds
for b6 being Function of b3,b2 holds (b6 | b4) | b5 = b6 | b5
proof end;

theorem Th80: :: TMAP_1:80
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b1,b2
for b6 being Function of b3,b2
for b7 being Function of b4,b2 st b4 = b1 & b5 = b7 holds
( b7 | b3 = b6 iff b5 | b3 = b6 ) by Def4;

theorem Th81: :: TMAP_1:81
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b3,b2
for b6 being Point of b3
for b7 being Point of b4 st b6 = b7 & b4 is SubSpace of b3 & b5 is_continuous_at b6 holds
b5 | b4 is_continuous_at b7
proof end;

theorem Th82: :: TMAP_1:82
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b1,b2 st b3 is SubSpace of b4 holds
for b6 being Point of b4
for b7 being Point of b3 st b6 = b7 & b5 | b4 is_continuous_at b6 holds
b5 | b3 is_continuous_at b7
proof end;

theorem Th83: :: TMAP_1:83
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b4,b2 st b3 is SubSpace of b4 holds
for b6 being Subset of b4
for b7 being Point of b4
for b8 being Point of b3 st b6 c= the carrier of b3 & b6 is a_neighborhood of b7 & b7 = b8 holds
( b5 is_continuous_at b7 iff b5 | b3 is_continuous_at b8 )
proof end;

theorem Th84: :: TMAP_1:84
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b4,b2 st b3 is SubSpace of b4 holds
for b6 being Subset of b4
for b7 being Point of b4
for b8 being Point of b3 st b6 is open & b7 in b6 & b6 c= the carrier of b3 & b7 = b8 holds
( b5 is_continuous_at b7 iff b5 | b3 is_continuous_at b8 )
proof end;

theorem Th85: :: TMAP_1:85
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b2
for b5 being Function of b4,b1 st b3 is SubSpace of b4 holds
for b6 being Subset of b2
for b7 being Point of b4
for b8 being Point of b3 st b6 is open & b7 in b6 & b6 c= the carrier of b3 & b7 = b8 holds
( b5 is_continuous_at b7 iff b5 | b3 is_continuous_at b8 )
proof end;

theorem Th86: :: TMAP_1:86
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b4,b2 st b3 is open SubSpace of b4 holds
for b6 being Point of b4
for b7 being Point of b3 st b6 = b7 holds
( b5 is_continuous_at b6 iff b5 | b3 is_continuous_at b7 )
proof end;

theorem Th87: :: TMAP_1:87
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b2
for b5 being Function of b4,b1 st b3 is open SubSpace of b2 & b3 is SubSpace of b4 holds
for b6 being Point of b4
for b7 being Point of b3 st b6 = b7 holds
( b5 is_continuous_at b6 iff b5 | b3 is_continuous_at b7 )
proof end;

theorem Th88: :: TMAP_1:88
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b4,b2 st TopStruct(# the carrier of b3,the topology of b3 #) = b4 holds
for b6 being Point of b4
for b7 being Point of b3 st b6 = b7 & b5 | b3 is_continuous_at b7 holds
b5 is_continuous_at b6
proof end;

theorem Th89: :: TMAP_1:89
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being continuous Function of b3,b2 st b4 is SubSpace of b3 holds
b5 | b4 is continuous Function of b4,b2
proof end;

theorem Th90: :: TMAP_1:90
for b1, b2 being non empty TopSpace
for b3, b4, b5 being non empty SubSpace of b1 st b3 is SubSpace of b4 & b5 is SubSpace of b3 holds
for b6 being Function of b4,b2 st b6 | b3 is continuous Function of b3,b2 holds
b6 | b5 is continuous Function of b5,b2
proof end;

theorem Th91: :: TMAP_1:91
for b1 being non empty 1-sorted
for b2 being Element of b1 holds (id b1) . b2 = b2
proof end;

theorem Th92: :: TMAP_1:92
for b1 being non empty 1-sorted
for b2 being Function of b1,b1 st ( for b3 being Element of b1 holds b2 . b3 = b3 ) holds
b2 = id b1
proof end;

theorem Th93: :: TMAP_1:93
for b1, b2 being non empty 1-sorted
for b3 being Function of the carrier of b1,the carrier of b2 holds
( b3 * (id b1) = b3 & (id b2) * b3 = b3 )
proof end;

theorem Th94: :: TMAP_1:94
for b1 being non empty TopSpace holds id b1 is continuous Function of b1,b1
proof end;

definition
let c1 be non empty TopSpace;
let c2 be SubSpace of c1;
canceled;
func incl c2 -> Function of a2,a1 equals :: TMAP_1:def 6
(id a1) | a2;
coherence
(id c1) | c2 is Function of c2,c1 ;
correctness
;
end;

:: deftheorem Def5 TMAP_1:def 5 :
canceled;

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

notation
let c1 be non empty TopSpace;
let c2 be SubSpace of c1;
synonym c2 incl c1 for incl c2;
end;

theorem Th95: :: TMAP_1:95
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1
for b3 being Point of b1 st b3 in the carrier of b2 holds
(incl b2) . b3 = b3
proof end;

theorem Th96: :: TMAP_1:96
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1
for b3 being Function of b2,b1 st ( for b4 being Point of b1 st b4 in the carrier of b2 holds
b4 = b3 . b4 ) holds
incl b2 = b3
proof end;

theorem Th97: :: TMAP_1:97
for b1, b2 being non empty TopSpace
for b3 being non empty SubSpace of b1
for b4 being Function of b1,b2 holds b4 | b3 = b4 * (incl b3)
proof end;

theorem Th98: :: TMAP_1:98
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1 holds incl b2 is continuous Function of b2,b1
proof end;

definition
let c1 be non empty TopSpace;
let c2 be Subset of c1;
func c2 -extension_of_the_topology_of c1 -> Subset-Family of a1 equals :: TMAP_1:def 7
{ (b1 \/ (b2 /\ a2)) where B is Subset of a1, B is Subset of a1 : ( b1 in the topology of a1 & b2 in the topology of a1 ) } ;
coherence
{ (b1 \/ (b2 /\ c2)) where B is Subset of c1, B is Subset of c1 : ( b1 in the topology of c1 & b2 in the topology of c1 ) } is Subset-Family of c1
proof end;
end;

:: deftheorem Def7 defines -extension_of_the_topology_of TMAP_1:def 7 :
for b1 being non empty TopSpace
for b2 being Subset of b1 holds b2 -extension_of_the_topology_of b1 = { (b3 \/ (b4 /\ b2)) where B is Subset of b1, B is Subset of b1 : ( b3 in the topology of b1 & b4 in the topology of b1 ) } ;

theorem Th99: :: TMAP_1:99
for b1 being non empty TopSpace
for b2 being Subset of b1 holds the topology of b1 c= b2 -extension_of_the_topology_of b1
proof end;

theorem Th100: :: TMAP_1:100
for b1 being non empty TopSpace
for b2 being Subset of b1 holds { (b3 /\ b2) where B is Subset of b1 : b3 in the topology of b1 } c= b2 -extension_of_the_topology_of b1
proof end;

theorem Th101: :: TMAP_1:101
for b1 being non empty TopSpace
for b2, b3, b4 being Subset of b1 st b3 in the topology of b1 & b4 in { (b5 /\ b2) where B is Subset of b1 : b5 in the topology of b1 } holds
( b3 \/ b4 in b2 -extension_of_the_topology_of b1 & b3 /\ b4 in b2 -extension_of_the_topology_of b1 )
proof end;

theorem Th102: :: TMAP_1:102
for b1 being non empty TopSpace
for b2 being Subset of b1 holds b2 in b2 -extension_of_the_topology_of b1
proof end;

theorem Th103: :: TMAP_1:103
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 in the topology of b1 iff the topology of b1 = b2 -extension_of_the_topology_of b1 )
proof end;

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

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

registration
let c1 be non empty TopSpace;
let c2 be Subset of c1;
cluster a1 modified_with_respect_to a2 -> non empty strict ;
coherence
not c1 modified_with_respect_to c2 is empty ;
end;

theorem Th104: :: TMAP_1:104
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( the carrier of (b1 modified_with_respect_to b2) = the carrier of b1 & the topology of (b1 modified_with_respect_to b2) = b2 -extension_of_the_topology_of b1 ) ;

theorem Th105: :: TMAP_1:105
for b1 being non empty TopSpace
for b2 being Subset of b1
for b3 being Subset of (b1 modified_with_respect_to b2) st b3 = b2 holds
b3 is open
proof end;

theorem Th106: :: TMAP_1:106
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 is open iff TopStruct(# the carrier of b1,the topology of b1 #) = b1 modified_with_respect_to b2 )
proof end;

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

:: deftheorem Def9 defines modid TMAP_1:def 9 :
for b1 being non empty TopSpace
for b2 being Subset of b1 holds modid b1,b2 = id the carrier of b1;

theorem Th107: :: TMAP_1:107
for b1 being non empty TopSpace
for b2 being Subset of b1 st b2 is open holds
modid b1,b2 = id b1 by GRCAT_1:def 11;

theorem Th108: :: TMAP_1:108
for b1 being non empty TopSpace
for b2 being Subset of b1
for b3 being Point of b1 st not b3 in b2 holds
modid b1,b2 is_continuous_at b3
proof end;

theorem Th109: :: TMAP_1:109
for b1 being non empty TopSpace
for b2 being Subset of b1
for b3 being non empty SubSpace of b1 st the carrier of b3 misses b2 holds
for b4 being Point of b3 holds (modid b1,b2) | b3 is_continuous_at b4
proof end;

theorem Th110: :: TMAP_1:110
for b1 being non empty TopSpace
for b2 being Subset of b1
for b3 being non empty SubSpace of b1 st the carrier of b3 = b2 holds
for b4 being Point of b3 holds (modid b1,b2) | b3 is_continuous_at b4
proof end;

theorem Th111: :: TMAP_1:111
for b1 being non empty TopSpace
for b2 being Subset of b1
for b3 being non empty SubSpace of b1 st the carrier of b3 misses b2 holds
(modid b1,b2) | b3 is continuous Function of b3,(b1 modified_with_respect_to b2)
proof end;

theorem Th112: :: TMAP_1:112
for b1 being non empty TopSpace
for b2 being Subset of b1
for b3 being non empty SubSpace of b1 st the carrier of b3 = b2 holds
(modid b1,b2) | b3 is continuous Function of b3,(b1 modified_with_respect_to b2)
proof end;

theorem Th113: :: TMAP_1:113
for b1 being non empty TopSpace
for b2 being Subset of b1 holds
( b2 is open iff modid b1,b2 is continuous Function of b1,(b1 modified_with_respect_to b2) )
proof end;

definition
let c1 be non empty TopSpace;
let c2 be SubSpace of c1;
func c1 modified_with_respect_to c2 -> strict TopSpace means :Def10: :: TMAP_1:def 10
for b1 being Subset of a1 st b1 = the carrier of a2 holds
a3 = a1 modified_with_respect_to b1;
existence
ex b1 being strict TopSpace st
for b2 being Subset of c1 st b2 = the carrier of c2 holds
b1 = c1 modified_with_respect_to b2
proof end;
uniqueness
for b1, b2 being strict TopSpace st ( for b3 being Subset of c1 st b3 = the carrier of c2 holds
b1 = c1 modified_with_respect_to b3 ) & ( for b3 being Subset of c1 st b3 = the carrier of c2 holds
b2 = c1 modified_with_respect_to b3 ) holds
b1 = b2
proof end;
end;

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

registration
let c1 be non empty TopSpace;
let c2 be SubSpace of c1;
cluster a1 modified_with_respect_to a2 -> non empty strict ;
coherence
not c1 modified_with_respect_to c2 is empty
proof end;
end;

theorem Th114: :: TMAP_1:114
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1 holds
( the carrier of (b1 modified_with_respect_to b2) = the carrier of b1 & ( for b3 being Subset of b1 st b3 = the carrier of b2 holds
the topology of (b1 modified_with_respect_to b2) = b3 -extension_of_the_topology_of b1 ) )
proof end;

theorem Th115: :: TMAP_1:115
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1
for b3 being SubSpace of b1 modified_with_respect_to b2 st the carrier of b3 = the carrier of b2 holds
b3 is open SubSpace of b1 modified_with_respect_to b2
proof end;

theorem Th116: :: TMAP_1:116
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1 holds
( b2 is open SubSpace of b1 iff TopStruct(# the carrier of b1,the topology of b1 #) = b1 modified_with_respect_to b2 )
proof end;

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

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

theorem Th117: :: TMAP_1:117
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1 st b2 is open SubSpace of b1 holds
modid b1,b2 = id b1
proof end;

theorem Th118: :: TMAP_1:118
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1 st b2 misses b3 holds
for b4 being Point of b3 holds (modid b1,b2) | b3 is_continuous_at b4
proof end;

theorem Th119: :: TMAP_1:119
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1
for b3 being Point of b2 holds (modid b1,b2) | b2 is_continuous_at b3
proof end;

theorem Th120: :: TMAP_1:120
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1 st b2 misses b3 holds
(modid b1,b2) | b3 is continuous Function of b3,(b1 modified_with_respect_to b2)
proof end;

theorem Th121: :: TMAP_1:121
for b1 being non empty TopSpace
for b2 being non empty SubSpace of b1 holds (modid b1,b2) | b2 is continuous Function of b2,(b1 modified_with_respect_to b2)
proof end;

theorem Th122: :: TMAP_1:122
for b1 being non empty TopSpace
for b2 being SubSpace of b1 holds
( b2 is open SubSpace of b1 iff modid b1,b2 is continuous Function of b1,(b1 modified_with_respect_to b2) )
proof end;

theorem Th123: :: TMAP_1:123
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of (b3 union b4),b2
for b6 being Point of b3
for b7 being Point of b4
for b8 being Point of (b3 union b4) st b8 = b6 & b8 = b7 holds
( b5 is_continuous_at b8 iff ( b5 | b3 is_continuous_at b6 & b5 | b4 is_continuous_at b7 ) )
proof end;

theorem Th124: :: TMAP_1:124
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2
for b4, b5 being non empty SubSpace of b1
for b6 being Point of (b4 union b5)
for b7 being Point of b4
for b8 being Point of b5 st b6 = b7 & b6 = b8 holds
( b3 | (b4 union b5) is_continuous_at b6 iff ( b3 | b4 is_continuous_at b7 & b3 | b5 is_continuous_at b8 ) )
proof end;

theorem Th125: :: TMAP_1:125
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2
for b4, b5 being non empty SubSpace of b1 st b1 = b4 union b5 holds
for b6 being Point of b1
for b7 being Point of b4
for b8 being Point of b5 st b6 = b7 & b6 = b8 holds
( b3 is_continuous_at b6 iff ( b3 | b4 is_continuous_at b7 & b3 | b5 is_continuous_at b8 ) )
proof end;

theorem Th126: :: TMAP_1:126
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1 st b3,b4 are_weakly_separated holds
for b5 being Function of (b3 union b4),b2 holds
( b5 is continuous Function of (b3 union b4),b2 iff ( b5 | b3 is continuous Function of b3,b2 & b5 | b4 is continuous Function of b4,b2 ) )
proof end;

theorem Th127: :: TMAP_1:127
for b1, b2 being non empty TopSpace
for b3, b4 being non empty closed SubSpace of b1
for b5 being Function of (b3 union b4),b2 holds
( b5 is continuous Function of (b3 union b4),b2 iff ( b5 | b3 is continuous Function of b3,b2 & b5 | b4 is continuous Function of b4,b2 ) )
proof end;

theorem Th128: :: TMAP_1:128
for b1, b2 being non empty TopSpace
for b3, b4 being non empty open SubSpace of b1
for b5 being Function of (b3 union b4),b2 holds
( b5 is continuous Function of (b3 union b4),b2 iff ( b5 | b3 is continuous Function of b3,b2 & b5 | b4 is continuous Function of b4,b2 ) )
proof end;

theorem Th129: :: TMAP_1:129
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1 st b3,b4 are_weakly_separated holds
for b5 being Function of b1,b2 holds
( b5 | (b3 union b4) is continuous Function of (b3 union b4),b2 iff ( b5 | b3 is continuous Function of b3,b2 & b5 | b4 is continuous Function of b4,b2 ) )
proof end;

theorem Th130: :: TMAP_1:130
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2
for b4, b5 being non empty closed SubSpace of b1 holds
( b3 | (b4 union b5) is continuous Function of (b4 union b5),b2 iff ( b3 | b4 is continuous Function of b4,b2 & b3 | b5 is continuous Function of b5,b2 ) )
proof end;

theorem Th131: :: TMAP_1:131
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2
for b4, b5 being non empty open SubSpace of b1 holds
( b3 | (b4 union b5) is continuous Function of (b4 union b5),b2 iff ( b3 | b4 is continuous Function of b4,b2 & b3 | b5 is continuous Function of b5,b2 ) )
proof end;

theorem Th132: :: TMAP_1:132
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2
for b4, b5 being non empty SubSpace of b1 st b1 = b4 union b5 & b4,b5 are_weakly_separated holds
( b3 is continuous Function of b1,b2 iff ( b3 | b4 is continuous Function of b4,b2 & b3 | b5 is continuous Function of b5,b2 ) )
proof end;

theorem Th133: :: TMAP_1:133
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2
for b4, b5 being non empty closed SubSpace of b1 st b1 = b4 union b5 holds
( b3 is continuous Function of b1,b2 iff ( b3 | b4 is continuous Function of b4,b2 & b3 | b5 is continuous Function of b5,b2 ) )
proof end;

theorem Th134: :: TMAP_1:134
for b1, b2 being non empty TopSpace
for b3 being Function of b1,b2
for b4, b5 being non empty open SubSpace of b1 st b1 = b4 union b5 holds
( b3 is continuous Function of b1,b2 iff ( b3 | b4 is continuous Function of b4,b2 & b3 | b5 is continuous Function of b5,b2 ) )
proof end;

theorem Th135: :: TMAP_1:135
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1 holds
( b2,b3 are_separated iff ( b2 misses b3 & ( for b4 being non empty TopSpace
for b5 being Function of (b2 union b3),b4 st b5 | b2 is continuous Function of b2,b4 & b5 | b3 is continuous Function of b3,b4 holds
b5 is continuous Function of (b2 union b3),b4 ) ) )
proof end;

theorem Th136: :: TMAP_1:136
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1 holds
( b2,b3 are_separated iff ( b2 misses b3 & ( for b4 being non empty TopSpace
for b5 being Function of b1,b4 st b5 | b2 is continuous Function of b2,b4 & b5 | b3 is continuous Function of b3,b4 holds
b5 | (b2 union b3) is continuous Function of (b2 union b3),b4 ) ) )
proof end;

theorem Th137: :: TMAP_1:137
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1 st b1 = b2 union b3 holds
( b2,b3 are_separated iff ( b2 misses b3 & ( for b4 being non empty TopSpace
for b5 being Function of b1,b4 st b5 | b2 is continuous Function of b2,b4 & b5 | b3 is continuous Function of b3,b4 holds
b5 is continuous Function of b1,b4 ) ) )
proof end;

definition
let c1, c2 be non empty TopSpace;
let c3, c4 be non empty SubSpace of c1;
let c5 be Function of c3,c2;
let c6 be Function of c4,c2;
assume E103: ( c3 misses c4 or c5 | (c3 meet c4) = c6 | (c3 meet c4) ) ;
func c5 union c6 -> Function of (a3 union a4),a2 means :Def12: :: TMAP_1:def 12
( a7 | a3 = a5 & a7 | a4 = a6 );
existence
ex b1 being Function of (c3 union c4),c2 st
( b1 | c3 = c5 & b1 | c4 = c6 )
proof end;
uniqueness
for b1, b2 being Function of (c3 union c4),c2 st b1 | c3 = c5 & b1 | c4 = c6 & b2 | c3 = c5 & b2 | c4 = c6 holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines union TMAP_1:def 12 :
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b3,b2
for b6 being Function of b4,b2 st ( b3 misses b4 or b5 | (b3 meet b4) = b6 | (b3 meet b4) ) holds
for b7 being Function of (b3 union b4),b2 holds
( b7 = b5 union b6 iff ( b7 | b3 = b5 & b7 | b4 = b6 ) );

theorem Th138: :: TMAP_1:138
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of (b3 union b4),b2 holds b5 = (b5 | b3) union (b5 | b4)
proof end;

theorem Th139: :: TMAP_1:139
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1 st b1 = b3 union b4 holds
for b5 being Function of b1,b2 holds b5 = (b5 | b3) union (b5 | b4)
proof end;

theorem Th140: :: TMAP_1:140
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1 st b3 meets b4 holds
for b5 being Function of b3,b2
for b6 being Function of b4,b2 holds
( ( (b5 union b6) | b3 = b5 & (b5 union b6) | b4 = b6 ) iff b5 | (b3 meet b4) = b6 | (b3 meet b4) )
proof end;

theorem Th141: :: TMAP_1:141
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b3,b2
for b6 being Function of b4,b2 st b5 | (b3 meet b4) = b6 | (b3 meet b4) holds
( ( b3 is SubSpace of b4 implies b5 union b6 = b6 ) & ( b5 union b6 = b6 implies b3 is SubSpace of b4 ) & ( b4 is SubSpace of b3 implies b5 union b6 = b5 ) & ( b5 union b6 = b5 implies b4 is SubSpace of b3 ) )
proof end;

theorem Th142: :: TMAP_1:142
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1
for b5 being Function of b3,b2
for b6 being Function of b4,b2 st ( b3 misses b4 or b5 | (b3 meet b4) = b6 | (b3 meet b4) ) holds
b5 union b6 = b6 union b5
proof end;

theorem Th143: :: TMAP_1:143
for b1, b2 being non empty TopSpace
for b3, b4, b5 being non empty SubSpace of b1
for b6 being Function of b3,b2
for b7 being Function of b4,b2
for b8 being Function of b5,b2 st ( b3 misses b4 or b6 | (b3 meet b4) = b7 | (b3 meet b4) ) & ( b3 misses b5 or b6 | (b3 meet b5) = b8 | (b3 meet b5) ) & ( b4 misses b5 or b7 | (b4 meet b5) = b8 | (b4 meet b5) ) holds
(b6 union b7) union b8 = b6 union (b7 union b8)
proof end;

theorem Th144: :: TMAP_1:144
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1 st b3 meets b4 holds
for b5 being continuous Function of b3,b2
for b6 being continuous Function of b4,b2 st b5 | (b3 meet b4) = b6 | (b3 meet b4) & b3,b4 are_weakly_separated holds
b5 union b6 is continuous Function of (b3 union b4),b2
proof end;

theorem Th145: :: TMAP_1:145
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1 st b3 misses b4 holds
for b5 being continuous Function of b3,b2
for b6 being continuous Function of b4,b2 st b3,b4 are_weakly_separated holds
b5 union b6 is continuous Function of (b3 union b4),b2
proof end;

theorem Th146: :: TMAP_1:146
for b1, b2 being non empty TopSpace
for b3, b4 being non empty closed SubSpace of b1 st b3 meets b4 holds
for b5 being continuous Function of b3,b2
for b6 being continuous Function of b4,b2 st b5 | (b3 meet b4) = b6 | (b3 meet b4) holds
b5 union b6 is continuous Function of (b3 union b4),b2
proof end;

theorem Th147: :: TMAP_1:147
for b1, b2 being non empty TopSpace
for b3, b4 being non empty open SubSpace of b1 st b3 meets b4 holds
for b5 being continuous Function of b3,b2
for b6 being continuous Function of b4,b2 st b5 | (b3 meet b4) = b6 | (b3 meet b4) holds
b5 union b6 is continuous Function of (b3 union b4),b2
proof end;

theorem Th148: :: TMAP_1:148
for b1, b2 being non empty TopSpace
for b3, b4 being non empty closed SubSpace of b1 st b3 misses b4 holds
for b5 being continuous Function of b3,b2
for b6 being continuous Function of b4,b2 holds b5 union b6 is continuous Function of (b3 union b4),b2
proof end;

theorem Th149: :: TMAP_1:149
for b1, b2 being non empty TopSpace
for b3, b4 being non empty open SubSpace of b1 st b3 misses b4 holds
for b5 being continuous Function of b3,b2
for b6 being continuous Function of b4,b2 holds b5 union b6 is continuous Function of (b3 union b4),b2
proof end;

theorem Th150: :: TMAP_1:150
for b1 being non empty TopSpace
for b2, b3 being non empty SubSpace of b1 holds
( b2,b3 are_separated iff ( b2 misses b3 & ( for b4 being non empty TopSpace
for b5 being continuous Function of b2,b4
for b6 being continuous Function of b3,b4 holds b5 union b6 is continuous Function of (b2 union b3),b4 ) ) )
proof end;

theorem Th151: :: TMAP_1:151
for b1, b2 being non empty TopSpace
for b3, b4 being non empty SubSpace of b1 st b1 = b3 union b4 holds
for b5 being continuous Function of b3,b2
for b6 being continuous Function of b4,b2 st (b5 union b6) | b3 = b5 & (b5 union b6) | b4 = b6 & b3,b4 are_weakly_separated holds
b5 union b6 is continuous Function of b1,b2
proof end;

theorem Th152: :: TMAP_1:152
for b1, b2 being non empty TopSpace
for b3, b4 being non empty closed SubSpace of b1
for b5 being continuous Function of b3,b2
for b6 being continuous Function of b4,b2 st b1 = b3 union b4 & (b5 union b6) | b3 = b5 & (b5 union b6) | b4 = b6 holds
b5 union b6 is continuous Function of b1,b2
proof end;

theorem Th153: :: TMAP_1:153
for b1, b2 being non empty TopSpace
for b3, b4 being non empty open SubSpace of b1
for b5 being continuous Function of b3,b2
for b6 being continuous Function of b4,b2 st b1 = b3 union b4 & (b5 union b6) | b3 = b5 & (b5 union b6) | b4 = b6 holds
b5 union b6 is continuous Function of b1,b2
proof end;