:: TOPMETR2 semantic presentation

theorem Th1: :: TOPMETR2:1

for x, y, z being real number st x <= y & y <= z holds
[.x,y.] /\ [.y,z.] = {y}

proof end;

theorem :: TOPMETR2:2

for f, g being Function st f is one-to-one & g is one-to-one & ( for x1, x2 being set st x1 in dom g & x2 in (dom f) \ (dom g) holds
g . x1 <> f . x2 ) holds
f +* g is one-to-one

proof end;

Lm1: for f, g being Function st f .: ((dom f) /\ (dom g)) c= rng g holds
(rng f) \ (rng g) c= rng (f +* g)

proof end;

theorem :: TOPMETR2:3

for f, g being Function st f .: ((dom f) /\ (dom g)) c= rng g holds
(rng f) \/ (rng g) = rng (f +* g)

proof end;

theorem Th4: :: TOPMETR2:4

for T, S being non empty TopSpace
for p being Point of T
for T1, T2 being SubSpace of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact & T2 is compact & T is_T2 & f is continuous & g is continuous & f . p = g . p holds
f +* g is continuous Function of T,S

proof end;

theorem :: TOPMETR2:5

for S, T being non empty TopSpace
for T1, T2 being SubSpace of T
for p1, p2 being Point of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is_T2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds
f +* g is continuous Function of T,S

proof end;

theorem :: TOPMETR2:6

for T being being_T2 TopSpace
for P, Q being Subset of T
for p being Point of T
for f being Function of I[01] ,(T | P)
for g being Function of I[01] ,(T | Q) st P /\ Q = {p} & f is_homeomorphism & f . 1 = p & g is_homeomorphism & g . 0 = p holds
ex h being Function of I[01] ,(T | (P \/ Q)) st
( h is_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 )

proof end;