let T be T_2 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 being_homeomorphism & f . 1 = p & g is being_homeomorphism & g . 0 = p holds
ex h being Function of I[01],(T | (P \/ Q)) st
( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 )
1 / 2 in { r where r is Real : ( 0 <= r & r <= 1 ) }
;
then reconsider pp = 1 / 2 as Point of I[01] by BORSUK_1:40, RCOMP_1:def 1;
reconsider PP = [.0,(1 / 2).] as Subset of R^1 by TOPMETR:17;
A1:
1 / 2 in [.0,1.]
by XXREAL_1:1;
1 in [.0,1.]
by XXREAL_1:1;
then
[.(1 / 2),1.] c= the carrier of I[01]
by A1, BORSUK_1:40, XXREAL_2:def 12;
then A2:
the carrier of (Closed-Interval-TSpace ((1 / 2),1)) c= the carrier of I[01]
by TOPMETR:18;
0 in [.0,1.]
by XXREAL_1:1;
then
[.0,(1 / 2).] c= the carrier of I[01]
by A1, BORSUK_1:40, XXREAL_2:def 12;
then
the carrier of (Closed-Interval-TSpace (0,(1 / 2))) c= the carrier of I[01]
by TOPMETR:18;
then reconsider T1 = Closed-Interval-TSpace (0,(1 / 2)), T2 = Closed-Interval-TSpace ((1 / 2),1) as SubSpace of I[01] by A2, TOPMETR:3;
deffunc H1( Real) -> Element of REAL = In ((2 * $1),REAL);
let P, Q be 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 being_homeomorphism & f . 1 = p & g is being_homeomorphism & g . 0 = p holds
ex h being Function of I[01],(T | (P \/ Q)) st
( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 )
let p be 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 being_homeomorphism & f . 1 = p & g is being_homeomorphism & g . 0 = p holds
ex h being Function of I[01],(T | (P \/ Q)) st
( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 )
let f be Function of I[01],(T | P); for g being Function of I[01],(T | Q) st P /\ Q = {p} & f is being_homeomorphism & f . 1 = p & g is being_homeomorphism & g . 0 = p holds
ex h being Function of I[01],(T | (P \/ Q)) st
( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 )
let g be Function of I[01],(T | Q); ( P /\ Q = {p} & f is being_homeomorphism & f . 1 = p & g is being_homeomorphism & g . 0 = p implies ex h being Function of I[01],(T | (P \/ Q)) st
( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 ) )
assume that
A3:
P /\ Q = {p}
and
A4:
f is being_homeomorphism
and
A5:
f . 1 = p
and
A6:
g is being_homeomorphism
and
A7:
g . 0 = p
; ex h being Function of I[01],(T | (P \/ Q)) st
( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 )
Q = [#] (T | Q)
by PRE_TOPC:def 5;
then A8:
rng g = Q
by A6, TOPS_2:def 5;
p in P /\ Q
by A3, TARSKI:def 1;
then reconsider M = T as non empty TopSpace ;
reconsider P9 = P, Q9 = Q as non empty Subset of M by A3;
reconsider R = P9 \/ Q9 as non empty Subset of M ;
A9:
M | P9 is SubSpace of M | R
by TOPMETR:4;
defpred S1[ object , object ] means for a being Real st a = $1 holds
$2 = f . (2 * a);
consider f3 being Function of REAL,REAL such that
A10:
for x being Element of REAL holds f3 . x = H1(x)
from FUNCT_2:sch 4();
A11: R =
[#] (M | R)
by PRE_TOPC:def 5
.=
the carrier of (M | R)
;
then
dom g = the carrier of I[01]
by FUNCT_2:def 1;
then reconsider g9 = g as Function of I[01],(M | R) by A8, A11, RELSET_1:4, XBOOLE_1:7;
A12:
M | Q9 is SubSpace of M | R
by TOPMETR:4;
g is continuous
by A6, TOPS_2:def 5;
then A13:
g9 is continuous
by A12, PRE_TOPC:26;
reconsider PP = PP as non empty Subset of R^1 by XXREAL_1:1;
A14:
( T1 is compact & T2 is compact )
by HEINE:4;
P = [#] (T | P)
by PRE_TOPC:def 5;
then A15:
rng f = P
by A4, TOPS_2:def 5;
dom f = the carrier of I[01]
by A11, FUNCT_2:def 1;
then reconsider ff = f as Function of I[01],(M | R) by A15, A11, RELSET_1:4, XBOOLE_1:7;
f is continuous
by A4, TOPS_2:def 5;
then A16:
ff is continuous
by A9, PRE_TOPC:26;
reconsider f3 = f3 as Function of R^1,R^1 by TOPMETR:17;
A17: dom (f3 | [.0,(1 / 2).]) =
(dom f3) /\ [.0,(1 / 2).]
by RELAT_1:61
.=
REAL /\ [.0,(1 / 2).]
by FUNCT_2:def 1
.=
[.0,(1 / 2).]
by XBOOLE_1:28
.=
the carrier of T1
by TOPMETR:18
;
rng (f3 | [.0,(1 / 2).]) c= the carrier of R^1
;
then reconsider f39 = f3 | PP as Function of T1,R^1 by A17, FUNCT_2:def 1, RELSET_1:4;
A18:
dom f39 = the carrier of T1
by FUNCT_2:def 1;
rng f39 c= the carrier of I[01]
then reconsider f4 = f39 as Function of T1,I[01] by A18, RELSET_1:4;
A24:
R^1 | PP = T1
by TOPMETR:19;
for x being Real holds f3 . x = (dwa * x) + 0
then
f39 is continuous
by A24, TOPMETR:7, TOPMETR:21;
then A25:
f4 is continuous
by PRE_TOPC:27;
reconsider PP = [.(1 / 2),1.] as Subset of R^1 by TOPMETR:17;
reconsider PP = PP as non empty Subset of R^1 by XXREAL_1:1;
deffunc H2( Real) -> Element of REAL = In (((2 * $1) - 1),REAL);
consider g3 being Function of REAL,REAL such that
A26:
for x being Element of REAL holds g3 . x = H2(x)
from FUNCT_2:sch 4();
reconsider g3 = g3 as Function of R^1,R^1 by TOPMETR:17;
A27: dom (g3 | [.(1 / 2),1.]) =
(dom g3) /\ [.(1 / 2),1.]
by RELAT_1:61
.=
REAL /\ [.(1 / 2),1.]
by FUNCT_2:def 1
.=
[.(1 / 2),1.]
by XBOOLE_1:28
.=
the carrier of T2
by TOPMETR:18
;
rng (g3 | [.(1 / 2),1.]) c= the carrier of R^1
;
then reconsider g39 = g3 | PP as Function of T2,R^1 by A27, FUNCT_2:def 1, RELSET_1:4;
A28:
dom g39 = the carrier of T2
by FUNCT_2:def 1;
rng g39 c= the carrier of I[01]
proof
let y be
object ;
TARSKI:def 3 ( not y in rng g39 or y in the carrier of I[01] )
assume
y in rng g39
;
y in the carrier of I[01]
then consider x being
object such that A29:
x in dom g39
and A30:
y = g39 . x
by FUNCT_1:def 3;
x in [.(1 / 2),1.]
by A28, A29, TOPMETR:18;
then
x in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
by RCOMP_1:def 1;
then consider r being
Real such that A31:
x = r
and A32:
1
/ 2
<= r
and A33:
r <= 1
;
2
* (1 / 2) <= 2
* r
by A32, XREAL_1:64;
then A34:
1
- 1
<= (2 * r) - 1
by XREAL_1:9;
2
* r <= 2
* 1
by A33, XREAL_1:64;
then A35:
(2 * r) - 1
<= (1 + 1) - 1
by XREAL_1:9;
reconsider r =
r as
Element of
REAL by XREAL_0:def 1;
y =
g3 . x
by A29, A30, FUNCT_1:47
.=
H2(
r)
by A26, A31
.=
(dwa * r) - 1
;
then
y in { rr where rr is Real : ( 0 <= rr & rr <= 1 ) }
by A34, A35;
hence
y in the
carrier of
I[01]
by BORSUK_1:40, RCOMP_1:def 1;
verum
end;
then reconsider g4 = g39 as Function of T2,I[01] by A28, RELSET_1:4;
( [#] T1 = [.0,(1 / 2).] & [#] T2 = [.(1 / 2),1.] )
by TOPMETR:18;
then A36:
( ([#] T1) \/ ([#] T2) = [#] I[01] & ([#] T1) /\ ([#] T2) = {pp} )
by BORSUK_1:40, XXREAL_1:165, XXREAL_1:418;
A37:
for x being Real holds g3 . x = (2 * x) + (- 1)
R^1 | PP = T2
by TOPMETR:19;
then
g39 is continuous
by A37, TOPMETR:7, TOPMETR:21;
then A38:
g4 is continuous
by PRE_TOPC:27;
A39:
for x being object st x in [.0,(1 / 2).] holds
ex u being object st S1[x,u]
consider f2 being Function such that
A41:
dom f2 = [.0,(1 / 2).]
and
A42:
for x being object st x in [.0,(1 / 2).] holds
S1[x,f2 . x]
from CLASSES1:sch 1(A39);
A43:
dom f2 = the carrier of T1
by A41, TOPMETR:18;
f is Function of the carrier of I[01], the carrier of (M | P9)
;
then A44:
dom f = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
now for y being object st y in rng f2 holds
y in Plet y be
object ;
( y in rng f2 implies y in P )assume
y in rng f2
;
y in Pthen consider x being
object such that A45:
x in dom f2
and A46:
y = f2 . x
by FUNCT_1:def 3;
x in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) }
by A41, A45, RCOMP_1:def 1;
then consider a being
Real such that A47:
x = a
and A48:
(
0 <= a &
a <= 1
/ 2 )
;
(
0 <= 2
* a & 2
* a <= 2
* (1 / 2) )
by A48, XREAL_1:64, XREAL_1:127;
then
2
* a in { r where r is Real : ( 0 <= r & r <= 1 ) }
;
then A49:
2
* a in dom f
by A44, RCOMP_1:def 1;
y = f . (2 * a)
by A41, A42, A45, A46, A47;
hence
y in P
by A15, A49, FUNCT_1:def 3;
verum end;
then A50:
rng f2 c= P
;
P c= P \/ Q
by XBOOLE_1:7;
then
rng f2 c= the carrier of (T | (P \/ Q))
by A11, A50;
then reconsider f1 = f2 as Function of T1,(M | R) by A43, FUNCT_2:def 1, RELSET_1:4;
for x being object st x in the carrier of T1 holds
f1 . x = (ff * f4) . x
then A52:
f1 is continuous
by A25, A16, FUNCT_2:12;
defpred S2[ object , object ] means for a being Real st a = $1 holds
$2 = g . ((2 * a) - 1);
A56:
for x being object st x in [.(1 / 2),1.] holds
ex u being object st S2[x,u]
consider g2 being Function such that
A58:
dom g2 = [.(1 / 2),1.]
and
A59:
for x being object st x in [.(1 / 2),1.] holds
S2[x,g2 . x]
from CLASSES1:sch 1(A56);
A60:
dom g2 = the carrier of T2
by A58, TOPMETR:18;
g is Function of the carrier of I[01], the carrier of (M | Q9)
;
then A61:
dom g = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
now for y being object st y in rng g2 holds
y in Qlet y be
object ;
( y in rng g2 implies y in Q )assume
y in rng g2
;
y in Qthen consider x being
object such that A62:
x in dom g2
and A63:
y = g2 . x
by FUNCT_1:def 3;
x in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) }
by A58, A62, RCOMP_1:def 1;
then consider a being
Real such that A64:
x = a
and A65:
1
/ 2
<= a
and A66:
a <= 1
;
2
* a <= 2
* 1
by A66, XREAL_1:64;
then A67:
(2 * a) - 1
<= (1 + 1) - 1
by XREAL_1:9;
2
* (1 / 2) = 1
;
then
1
<= 2
* a
by A65, XREAL_1:64;
then
1
- 1
<= (2 * a) - 1
by XREAL_1:9;
then
(2 * a) - 1
in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A67;
then A68:
(2 * a) - 1
in dom g
by A61, RCOMP_1:def 1;
y = g . ((2 * a) - 1)
by A58, A59, A62, A63, A64;
hence
y in Q
by A8, A68, FUNCT_1:def 3;
verum end;
then A69:
rng g2 c= Q
;
A70:
Q c= rng g2
proof
let a be
object ;
TARSKI:def 3 ( not a in Q or a in rng g2 )
assume
a in Q
;
a in rng g2
then consider x being
object such that A71:
x in dom g
and A72:
a = g . x
by A8, FUNCT_1:def 3;
x in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A61, A71, RCOMP_1:def 1;
then consider x9 being
Real such that A73:
x9 = x
and A74:
0 <= x9
and A75:
x9 <= 1
;
x9 + 1
<= 1
+ 1
by A75, XREAL_1:6;
then A76:
(x9 + 1) / 2
<= 2
/ 2
by XREAL_1:72;
0 + 1
<= x9 + 1
by A74, XREAL_1:6;
then
1
/ 2
<= (x9 + 1) / 2
by XREAL_1:72;
then
(x9 + 1) / 2
in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
by A76;
then A77:
(x9 + 1) / 2
in dom g2
by A58, RCOMP_1:def 1;
a =
g . ((2 * ((x9 + 1) / 2)) - 1)
by A72, A73
.=
g2 . ((x9 + 1) / 2)
by A58, A59, A77
;
hence
a in rng g2
by A77, FUNCT_1:def 3;
verum
end;
TopSpaceMetr RealSpace is T_2
by PCOMPS_1:34;
then A78:
I[01] is T_2
by TOPMETR:2, TOPMETR:def 6;
A79:
1 / 2 in [.(1 / 2),1.]
by XXREAL_1:1;
Q c= P \/ Q
by XBOOLE_1:7;
then
rng g2 c= the carrier of (M | R)
by A11, A69;
then reconsider g1 = g2 as Function of T2,(M | R) by A60, FUNCT_2:def 1, RELSET_1:4;
for x being object st x in the carrier of T2 holds
g1 . x = (g9 * g4) . x
then A86:
g1 is continuous
by A38, A13, FUNCT_2:12;
1 / 2 in [.0,(1 / 2).]
by XXREAL_1:1;
then f1 . pp =
g . ((2 * (1 / 2)) - 1)
by A5, A7, A42
.=
g1 . pp
by A59, A79
;
then reconsider h = f2 +* g2 as continuous Function of I[01],(M | R) by A36, A14, A78, A52, A86, COMPTS_1:20;
A87:
g is one-to-one
by A6, TOPS_2:def 5;
A88:
f is one-to-one
by A4, TOPS_2:def 5;
now for x1, x2 being object st x1 in dom h & x2 in dom h & h . x1 = h . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in dom h & x2 in dom h & h . x1 = h . x2 implies x1 = x2 )assume that A89:
x1 in dom h
and A90:
x2 in dom h
and A91:
h . x1 = h . x2
;
x1 = x2now x1 = x2per cases
( ( not x1 in dom g2 & not x2 in dom g2 ) or ( not x1 in dom g2 & x2 in dom g2 ) or ( x1 in dom g2 & not x2 in dom g2 ) or ( x1 in dom g2 & x2 in dom g2 ) )
;
suppose A92:
( not
x1 in dom g2 & not
x2 in dom g2 )
;
x1 = x2A93:
dom h = (dom f2) \/ (dom g2)
by FUNCT_4:def 1;
then
x1 in [.0,(1 / 2).]
by A41, A89, A92, XBOOLE_0:def 3;
then
x1 in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) }
by RCOMP_1:def 1;
then consider x19 being
Real such that A94:
x19 = x1
and
0 <= x19
and
x19 <= 1
/ 2
;
reconsider x19 =
x19 as
Real ;
A95:
x1 in dom f2
by A89, A92, A93, XBOOLE_0:def 3;
then A96:
2
* x19 in dom f
by A53, A94;
x2 in [.0,(1 / 2).]
by A41, A90, A92, A93, XBOOLE_0:def 3;
then
x2 in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) }
by RCOMP_1:def 1;
then consider x29 being
Real such that A97:
x29 = x2
and
0 <= x29
and
x29 <= 1
/ 2
;
reconsider x29 =
x29 as
Real ;
A98:
x2 in dom f2
by A90, A92, A93, XBOOLE_0:def 3;
then A99:
2
* x29 in dom f
by A53, A97;
f . (2 * x19) =
f2 . x1
by A41, A42, A95, A94
.=
h . x2
by A91, A92, FUNCT_4:11
.=
f2 . x2
by A92, FUNCT_4:11
.=
f . (2 * x29)
by A41, A42, A98, A97
;
then
2
* x19 = 2
* x29
by A88, A96, A99, FUNCT_1:def 4;
hence
x1 = x2
by A94, A97;
verum end; suppose A100:
( not
x1 in dom g2 &
x2 in dom g2 )
;
x1 = x2
dom h = (dom f2) \/ (dom g2)
by FUNCT_4:def 1;
then A101:
x1 in dom f2
by A89, A100, XBOOLE_0:def 3;
then
x1 in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) }
by A41, RCOMP_1:def 1;
then consider x19 being
Real such that A102:
x19 = x1
and
0 <= x19
and
x19 <= 1
/ 2
;
reconsider x19 =
x19 as
Real ;
A103:
2
* x19 in dom f
by A53, A101, A102;
then A104:
f . (2 * x19) in P
by A15, FUNCT_1:def 3;
x2 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) }
by A58, A100, RCOMP_1:def 1;
then consider x29 being
Real such that A105:
x29 = x2
and
1
/ 2
<= x29
and
x29 <= 1
;
reconsider x29 =
x29 as
Real ;
A106:
(2 * x29) - 1
in dom g
by A80, A100, A105;
then A107:
g . ((2 * x29) - 1) in Q
by A8, FUNCT_1:def 3;
A108:
1
in dom f
by A44, XXREAL_1:1;
A109:
0 in dom g
by A61, XXREAL_1:1;
A110:
f . (2 * x19) =
f2 . x1
by A41, A42, A101, A102
.=
h . x2
by A91, A100, FUNCT_4:11
.=
g2 . x2
by A100, FUNCT_4:13
.=
g . ((2 * x29) - 1)
by A58, A59, A100, A105
;
then
g . ((2 * x29) - 1) in P /\ Q
by A104, A107, XBOOLE_0:def 4;
then
g . ((2 * x29) - 1) = p
by A3, TARSKI:def 1;
then A111:
((2 * x29) - 1) + 1
= 0 + 1
by A7, A87, A106, A109, FUNCT_1:def 4;
f . (2 * x19) in P /\ Q
by A110, A104, A107, XBOOLE_0:def 4;
then
f . (2 * x19) = p
by A3, TARSKI:def 1;
then
(1 / 2) * (2 * x19) = (1 / 2) * 1
by A5, A88, A103, A108, FUNCT_1:def 4;
hence
x1 = x2
by A105, A102, A111;
verum end; suppose A112:
(
x1 in dom g2 & not
x2 in dom g2 )
;
x1 = x2
dom h = (dom f2) \/ (dom g2)
by FUNCT_4:def 1;
then A113:
x2 in dom f2
by A90, A112, XBOOLE_0:def 3;
then
x2 in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) }
by A41, RCOMP_1:def 1;
then consider x29 being
Real such that A114:
x29 = x2
and
0 <= x29
and
x29 <= 1
/ 2
;
reconsider x29 =
x29 as
Real ;
A115:
2
* x29 in dom f
by A53, A113, A114;
then A116:
f . (2 * x29) in P
by A15, FUNCT_1:def 3;
x1 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) }
by A58, A112, RCOMP_1:def 1;
then consider x19 being
Real such that A117:
x19 = x1
and
1
/ 2
<= x19
and
x19 <= 1
;
reconsider x19 =
x19 as
Real ;
A118:
(2 * x19) - 1
in dom g
by A80, A112, A117;
then A119:
g . ((2 * x19) - 1) in Q
by A8, FUNCT_1:def 3;
A120:
1
in dom f
by A44, XXREAL_1:1;
A121:
0 in dom g
by A61, XXREAL_1:1;
A122:
f . (2 * x29) =
f2 . x2
by A41, A42, A113, A114
.=
h . x1
by A91, A112, FUNCT_4:11
.=
g2 . x1
by A112, FUNCT_4:13
.=
g . ((2 * x19) - 1)
by A58, A59, A112, A117
;
then
g . ((2 * x19) - 1) in P /\ Q
by A116, A119, XBOOLE_0:def 4;
then
g . ((2 * x19) - 1) = p
by A3, TARSKI:def 1;
then A123:
((2 * x19) - 1) + 1
= 0 + 1
by A7, A87, A118, A121, FUNCT_1:def 4;
f . (2 * x29) in P /\ Q
by A122, A116, A119, XBOOLE_0:def 4;
then
f . (2 * x29) = p
by A3, TARSKI:def 1;
then
(1 / 2) * (2 * x29) = (1 / 2) * 1
by A5, A88, A115, A120, FUNCT_1:def 4;
hence
x1 = x2
by A117, A114, A123;
verum end; suppose A124:
(
x1 in dom g2 &
x2 in dom g2 )
;
x1 = x2then
x2 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) }
by A58, RCOMP_1:def 1;
then consider x29 being
Real such that A125:
x29 = x2
and
1
/ 2
<= x29
and
x29 <= 1
;
reconsider x29 =
x29 as
Real ;
A126:
(2 * x29) - 1
in dom g
by A80, A124, A125;
x1 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) }
by A58, A124, RCOMP_1:def 1;
then consider x19 being
Real such that A127:
x19 = x1
and
1
/ 2
<= x19
and
x19 <= 1
;
reconsider x19 =
x19 as
Real ;
A128:
(2 * x19) - 1
in dom g
by A80, A124, A127;
g . ((2 * x19) - 1) =
g2 . x1
by A58, A59, A124, A127
.=
h . x2
by A91, A124, FUNCT_4:13
.=
g2 . x2
by A124, FUNCT_4:13
.=
g . ((2 * x29) - 1)
by A58, A59, A124, A125
;
then
((2 * x19) - 1) + 1
= ((2 * x29) - 1) + 1
by A87, A128, A126, FUNCT_1:def 4;
hence
x1 = x2
by A127, A125;
verum end; end; end; hence
x1 = x2
;
verum end;
then A129:
( dom h = [#] I[01] & h is one-to-one )
by FUNCT_1:def 4, FUNCT_2:def 1;
reconsider h9 = h as Function of I[01],(T | (P \/ Q)) ;
take
h9
; ( h9 is being_homeomorphism & h9 . 0 = f . 0 & h9 . 1 = g . 1 )
A130:
0 in [.0,(1 / 2).]
by XXREAL_1:1;
A131:
P c= rng f2
A137:
P c= rng h
proof
let a be
object ;
TARSKI:def 3 ( not a in P or a in rng h )
assume
a in P
;
a in rng h
then consider x being
object such that A138:
x in dom f2
and A139:
a = f2 . x
by A131, FUNCT_1:def 3;
now a in rng hper cases
( x in [.(1 / 2),1.] or not x in [.(1 / 2),1.] )
;
suppose A140:
x in [.(1 / 2),1.]
;
a in rng hthen
x in [.0,(1 / 2).] /\ [.(1 / 2),1.]
by A41, A138, XBOOLE_0:def 4;
then
x in {(1 / 2)}
by XXREAL_1:418;
then A141:
x = 1
/ 2
by TARSKI:def 1;
x in (dom f2) \/ (dom g2)
by A138, XBOOLE_0:def 3;
then A142:
x in dom h
by FUNCT_4:def 1;
A143:
1
/ 2
in [.0,(1 / 2).]
by XXREAL_1:1;
h . x =
g2 . x
by A58, A140, FUNCT_4:13
.=
g . ((2 * (1 / 2)) - 1)
by A59, A140, A141
.=
f2 . (1 / 2)
by A5, A7, A42, A143
;
hence
a in rng h
by A139, A141, A142, FUNCT_1:def 3;
verum end; end; end;
hence
a in rng h
;
verum
end;
( rng h c= (rng f2) \/ (rng g2) & (rng f2) \/ (rng g2) c= P \/ Q )
by A50, A69, FUNCT_4:17, XBOOLE_1:13;
then A147:
rng h c= P \/ Q
;
rng g2 c= rng h
by FUNCT_4:18;
then
Q c= rng h
by A70;
then
P \/ Q c= rng h
by A137, XBOOLE_1:8;
then
rng h = P \/ Q
by A147, XBOOLE_0:def 10;
then A148:
rng h = [#] (M | R)
by PRE_TOPC:def 5;
( I[01] is compact & M | R is T_2 )
by HEINE:4, TOPMETR:2, TOPMETR:20;
hence
h9 is being_homeomorphism
by A148, A129, COMPTS_1:17; ( h9 . 0 = f . 0 & h9 . 1 = g . 1 )
not 0 in dom g2
by A58, XXREAL_1:1;
hence h9 . 0 =
f2 . 0
by FUNCT_4:11
.=
f . (2 * 0)
by A42, A130
.=
f . 0
;
h9 . 1 = g . 1
A149:
1 in dom g2
by A58, XXREAL_1:1;
hence h9 . 1 =
g2 . 1
by FUNCT_4:13
.=
g . ((2 * 1) - 1)
by A58, A59, A149
.=
g . 1
;
verum