:: TMAP_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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;

theorem Th1: :: TMAP_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty set
for f being Function of A,B
for A0 being Subset of A
for B0 being Subset of B holds
( f .: A0 c= B0 iff A0 c= f " B0 )
proof end;

theorem Th2: :: TMAP_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty set
for f being Function of A,B
for A0 being non empty Subset of A
for f0 being Function of A0,B st ( for c being Element of A st c in A0 holds
f . c = f0 . c ) holds
f | A0 = f0
proof end;

theorem :: TMAP_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: TMAP_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function
for A0, C being set st C c= A0 holds
f .: C = (f | A0) .: C
proof end;

theorem Th5: :: TMAP_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function
for A0, D being set st f " D c= A0 holds
f " D = (f | A0) " D
proof 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 Th6: :: TMAP_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th7: :: TMAP_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

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

theorem Th11: :: TMAP_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th12: :: TMAP_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th13: :: TMAP_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th14: :: TMAP_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th15: :: TMAP_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th16: :: TMAP_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th17: :: TMAP_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th19: :: TMAP_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th20: :: TMAP_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th21: :: TMAP_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th22: :: TMAP_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th23: :: TMAP_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th24: :: TMAP_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th27: :: TMAP_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th29: :: TMAP_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th31: :: TMAP_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th32: :: TMAP_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th33: :: TMAP_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th34: :: TMAP_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th35: :: TMAP_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th36: :: TMAP_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th37: :: TMAP_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th38: :: TMAP_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th39: :: TMAP_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th43: :: TMAP_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th44: :: TMAP_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th46: :: TMAP_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

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 Th47: :: TMAP_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th48: :: TMAP_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th49: :: TMAP_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th50: :: TMAP_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th51: :: TMAP_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th52: :: TMAP_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th49;

theorem Th56: :: TMAP_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

definition
let X, Y be non empty TopSpace;
let X0 be SubSpace of X;
let f be Function of X,Y;
func f | X0 -> Function of X0,Y equals :: TMAP_1:def 3
f | the carrier of X0;
coherence
f | the carrier of X0 is Function of X0,Y
proof end;
end;

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

theorem Th58: :: TMAP_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y, X being non empty TopSpace
for X0 being non empty SubSpace of X
for f being Function of X,Y
for x being Point of X st x in the carrier of X0 holds
f . x = (f | X0) . x by FUNCT_1:72;

theorem Th59: :: TMAP_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th60: :: TMAP_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th61: :: TMAP_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th4;

theorem :: TMAP_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th5;

theorem Th63: :: TMAP_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th64: :: TMAP_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem Th65: :: TMAP_1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th66: :: TMAP_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem Th68: :: TMAP_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty TopSpace
for f being continuous Function of X,Y
for X0 being non empty SubSpace of X holds f | X0 is continuous Function of X0,Y
proof end;

theorem Th69: :: TMAP_1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th70: :: TMAP_1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th70;

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 :Def4: :: TMAP_1:def 4
g | the carrier of X1;
coherence
g | the carrier of X1 is Function of X1,Y
proof end;
end;

:: deftheorem Def4 defines | TMAP_1:def 4 :
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 Th72: :: TMAP_1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th74: :: TMAP_1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th75: :: TMAP_1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th77: :: TMAP_1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th78: :: TMAP_1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th79: :: TMAP_1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th80: :: TMAP_1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Def4;

theorem Th81: :: TMAP_1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th82: :: TMAP_1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem Th83: :: TMAP_1:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th84: :: TMAP_1:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th86: :: TMAP_1:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th88: :: TMAP_1:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th89: :: TMAP_1:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th90: :: TMAP_1:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem Th91: :: TMAP_1:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty 1-sorted
for x being Element of X holds (id X) . x = x
proof end;

theorem :: TMAP_1:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty 1-sorted
for f being Function of X,X st ( for x being Element of X holds f . x = x ) holds
f = id X
proof end;

theorem Th93: :: TMAP_1:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty 1-sorted
for f being Function of the carrier of X,the carrier of Y holds
( f * (id X) = f & (id Y) * f = f )
proof end;

theorem Th94: :: TMAP_1:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace holds id X is continuous Function of X,X
proof end;

definition
let X be non empty TopSpace;
let X0 be SubSpace of X;
canceled;
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 TMAP_1:def 5 :
canceled;

:: 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:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds incl X0 is continuous Function of X0,X
proof end;

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 Th99: :: TMAP_1:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th100: :: TMAP_1:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th101: :: TMAP_1:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th102: :: TMAP_1:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th103: :: TMAP_1:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th105: :: TMAP_1:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th106: :: TMAP_1:106  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th107: :: TMAP_1:107  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for A being Subset of X st A is open holds
modid X,A = id X by GRCAT_1:def 11;

theorem Th108: :: TMAP_1:108  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th109: :: TMAP_1:109  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th110: :: TMAP_1:110  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th111: :: TMAP_1:111  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th112: :: TMAP_1:112  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th113: :: TMAP_1:113  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th114: :: TMAP_1:114  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:115  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:116  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:117  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty TopSpace
for X0 being non empty SubSpace of X st X0 is open SubSpace of X holds
modid X,X0 = id X
proof end;

theorem Th118: :: TMAP_1:118  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th119: :: TMAP_1:119  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:120  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:121  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:122  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem Th123: :: TMAP_1:123  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:124  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:125  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem Th126: :: TMAP_1:126  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th127: :: TMAP_1:127  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th128: :: TMAP_1:128  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th129: :: TMAP_1:129  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:130  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:131  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th132: :: TMAP_1:132  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th133: :: TMAP_1:133  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th134: :: TMAP_1:134  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem Th135: :: TMAP_1:135  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th136: :: TMAP_1:136  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:137  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

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 Th138: :: TMAP_1:138  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:139  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th140: :: TMAP_1:140  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:141  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:142  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:143  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: TMAP_1:144  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th145: :: TMAP_1:145  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:146  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:147  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:148  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:149  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: TMAP_1:150  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;

theorem :: TMAP_1:151  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:152  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:153  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;