let T be T_2 TopSpace; :: thesis: 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 ;
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 ;
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 ;
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 ;
deffunc H1( Real) -> Element of REAL = In ((2 * \$1),REAL);
let P, Q be Subset of T; :: thesis: 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; :: thesis: 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); :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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 ;
p in P /\ Q by ;
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 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 ;
A12: M | Q9 is SubSpace of M | R by TOPMETR:4;
g is continuous by ;
then A13: g9 is continuous by ;
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 ;
dom f = the carrier of I[01] by ;
then reconsider ff = f as Function of I[01],(M | R) by ;
f is continuous by ;
then A16: ff is continuous by ;
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 ;
A18: dom f39 = the carrier of T1 by FUNCT_2:def 1;
rng f39 c= the carrier of I[01]
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f39 or y in the carrier of I[01] )
assume y in rng f39 ; :: thesis: y in the carrier of I[01]
then consider x being object such that
A19: x in dom f39 and
A20: y = f39 . x by FUNCT_1:def 3;
x in [.0,(1 / 2).] by ;
then x in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } by RCOMP_1:def 1;
then consider r being Real such that
A21: x = r and
A22: ( 0 <= r & r <= 1 / 2 ) ;
A23: ( 2 * 0 <= 2 * r & 2 * r <= 2 * (1 / 2) ) by ;
reconsider r = r as Element of REAL by XREAL_0:def 1;
y = f3 . x by
.= H1(r) by ;
then y in { rr where rr is Real : ( 0 <= rr & rr <= 1 ) } by A23;
hence y in the carrier of I[01] by ; :: thesis: verum
end;
then reconsider f4 = f39 as Function of T1,I[01] by ;
A24: R^1 | PP = T1 by TOPMETR:19;
for x being Real holds f3 . x = (dwa * x) + 0
proof
let x be Real; :: thesis: f3 . x = (dwa * x) + 0
reconsider x = x as Element of REAL by XREAL_0:def 1;
f3 . x = H1(x) + 0 by A10;
hence f3 . x = (dwa * x) + 0 ; :: thesis: verum
end;
then f39 is continuous by ;
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 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 ;
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 ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g39 or y in the carrier of I[01] )
assume y in rng g39 ; :: thesis: 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 ;
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 ;
then A34: 1 - 1 <= (2 * r) - 1 by XREAL_1:9;
2 * r <= 2 * 1 by ;
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
.= H2(r) by
.= (dwa * r) - 1 ;
then y in { rr where rr is Real : ( 0 <= rr & rr <= 1 ) } by ;
hence y in the carrier of I[01] by ; :: thesis: verum
end;
then reconsider g4 = g39 as Function of T2,I[01] by ;
( [#] T1 = [.0,(1 / 2).] & [#] T2 = [.(1 / 2),1.] ) by TOPMETR:18;
then A36: ( ([#] T1) \/ ([#] T2) = [#] I[01] & ([#] T1) /\ ([#] T2) = {pp} ) by ;
A37: for x being Real holds g3 . x = (2 * x) + (- 1)
proof
let x be Real; :: thesis: g3 . x = (2 * x) + (- 1)
reconsider x = x as Element of REAL by XREAL_0:def 1;
g3 . x = H2(x) by A26
.= (dwa * x) - 1
.= (2 * x) + (- 1) ;
hence g3 . x = (2 * x) + (- 1) ; :: thesis: verum
end;
R^1 | PP = T2 by TOPMETR:19;
then g39 is continuous by ;
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]
proof
let x be object ; :: thesis: ( x in [.0,(1 / 2).] implies ex u being object st S1[x,u] )
assume x in [.0,(1 / 2).] ; :: thesis: ex u being object st S1[x,u]
then x in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } by RCOMP_1:def 1;
then consider r being Real such that
A40: r = x and
0 <= r and
r <= 1 / 2 ;
take f . (2 * r) ; :: thesis: S1[x,f . (2 * r)]
thus S1[x,f . (2 * r)] by A40; :: thesis: verum
end;
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 A43: dom f2 = the carrier of T1 by ;
f is Function of the carrier of I[01], the carrier of (M | P9) ;
then A44: dom f = [.0,1.] by ;
now :: thesis: for y being object st y in rng f2 holds
y in P
let y be object ; :: thesis: ( y in rng f2 implies y in P )
assume y in rng f2 ; :: thesis: y in P
then 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 ;
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 ;
then 2 * a in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then A49: 2 * a in dom f by ;
y = f . (2 * a) by A41, A42, A45, A46, A47;
hence y in P by ; :: thesis: 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 ;
then reconsider f1 = f2 as Function of T1,(M | R) by ;
for x being object st x in the carrier of T1 holds
f1 . x = (ff * f4) . x
proof
let x be object ; :: thesis: ( x in the carrier of T1 implies f1 . x = (ff * f4) . x )
assume A51: x in the carrier of T1 ; :: thesis: f1 . x = (ff * f4) . x
the carrier of T1 = [.0,(1 / 2).] by TOPMETR:18;
then reconsider x9 = x as Element of REAL by A51;
the carrier of T1 = [.0,(1 / 2).] by TOPMETR:18;
hence f1 . x = f . (2 * x9) by
.= f . H1(x9)
.= f . (f3 . x9) by A10
.= f . (f4 . x) by
.= (ff * f4) . x by ;
:: thesis: verum
end;
then A52: f1 is continuous by ;
A53: now :: thesis: for x being Real st x in dom f2 holds
2 * x in dom f
let x be Real; :: thesis: ( x in dom f2 implies 2 * x in dom f )
assume x in dom f2 ; :: thesis: 2 * x in dom f
then x in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by ;
then consider a being Real such that
A54: a = x and
A55: ( 0 <= a & a <= 1 / 2 ) ;
( 0 <= 2 * a & 2 * a <= 2 * (1 / 2) ) by ;
then 2 * a in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
hence 2 * x in dom f by ; :: thesis: verum
end;
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]
proof
let x be object ; :: thesis: ( x in [.(1 / 2),1.] implies ex u being object st S2[x,u] )
assume x in [.(1 / 2),1.] ; :: thesis: ex u being object st S2[x,u]
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
A57: r = x and
1 / 2 <= r and
r <= 1 ;
take g . ((2 * r) - 1) ; :: thesis: S2[x,g . ((2 * r) - 1)]
thus S2[x,g . ((2 * r) - 1)] by A57; :: thesis: verum
end;
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 A60: dom g2 = the carrier of T2 by ;
g is Function of the carrier of I[01], the carrier of (M | Q9) ;
then A61: dom g = [.0,1.] by ;
now :: thesis: for y being object st y in rng g2 holds
y in Q
let y be object ; :: thesis: ( y in rng g2 implies y in Q )
assume y in rng g2 ; :: thesis: y in Q
then 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 ;
then consider a being Real such that
A64: x = a and
A65: 1 / 2 <= a and
A66: a <= 1 ;
2 * a <= 2 * 1 by ;
then A67: (2 * a) - 1 <= (1 + 1) - 1 by XREAL_1:9;
2 * (1 / 2) = 1 ;
then 1 <= 2 * a by ;
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 ;
y = g . ((2 * a) - 1) by A58, A59, A62, A63, A64;
hence y in Q by ; :: thesis: verum
end;
then A69: rng g2 c= Q ;
A70: Q c= rng g2
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Q or a in rng g2 )
assume a in Q ; :: thesis: a in rng g2
then consider x being object such that
A71: x in dom g and
A72: a = g . x by ;
x in { r where r is Real : ( 0 <= r & r <= 1 ) } by ;
then consider x9 being Real such that
A73: x9 = x and
A74: 0 <= x9 and
A75: x9 <= 1 ;
x9 + 1 <= 1 + 1 by ;
then A76: (x9 + 1) / 2 <= 2 / 2 by XREAL_1:72;
0 + 1 <= x9 + 1 by ;
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 ;
a = g . ((2 * ((x9 + 1) / 2)) - 1) by
.= g2 . ((x9 + 1) / 2) by ;
hence a in rng g2 by ; :: thesis: verum
end;
TopSpaceMetr RealSpace is T_2 by PCOMPS_1:34;
then A78: I[01] is T_2 by ;
A79: 1 / 2 in [.(1 / 2),1.] by XXREAL_1:1;
A80: now :: thesis: for x being Real st x in dom g2 holds
(2 * x) - 1 in dom g
let x be Real; :: thesis: ( x in dom g2 implies (2 * x) - 1 in dom g )
assume x in dom g2 ; :: thesis: (2 * x) - 1 in dom g
then x in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by ;
then consider a being Real such that
A81: a = x and
A82: 1 / 2 <= a and
A83: a <= 1 ;
2 * a <= 2 * 1 by ;
then A84: (2 * a) - 1 <= (1 + 1) - 1 by XREAL_1:9;
2 * (1 / 2) = 1 ;
then 1 <= 2 * a by ;
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 A84;
hence (2 * x) - 1 in dom g by ; :: thesis: verum
end;
Q c= P \/ Q by XBOOLE_1:7;
then rng g2 c= the carrier of (M | R) by ;
then reconsider g1 = g2 as Function of T2,(M | R) by ;
for x being object st x in the carrier of T2 holds
g1 . x = (g9 * g4) . x
proof
let x be object ; :: thesis: ( x in the carrier of T2 implies g1 . x = (g9 * g4) . x )
assume A85: x in the carrier of T2 ; :: thesis: g1 . x = (g9 * g4) . x
the carrier of T2 = [.(1 / 2),1.] by TOPMETR:18;
then reconsider x9 = x as Element of REAL by A85;
the carrier of T2 = [.(1 / 2),1.] by TOPMETR:18;
hence g1 . x = g . ((2 * x9) - 1) by
.= g . H2(x9)
.= g . (g3 . x9) by A26
.= g . (g4 . x) by
.= (g9 * g4) . x by ;
:: thesis: verum
end;
then A86: g1 is continuous by ;
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 ;
then reconsider h = f2 +* g2 as continuous Function of I[01],(M | R) by ;
A87: g is one-to-one by ;
A88: f is one-to-one by ;
now :: thesis: for x1, x2 being object st x1 in dom h & x2 in dom h & h . x1 = h . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( 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 ; :: thesis: x1 = x2
now :: thesis: x1 = x2
per 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 ) ; :: thesis: x1 = x2
A93: dom h = (dom f2) \/ (dom g2) by FUNCT_4:def 1;
then x1 in [.0,(1 / 2).] by ;
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 ;
then A96: 2 * x19 in dom f by ;
x2 in [.0,(1 / 2).] by ;
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 ;
then A99: 2 * x29 in dom f by ;
f . (2 * x19) = f2 . x1 by A41, A42, A95, A94
.= h . x2 by
.= f2 . x2 by
.= f . (2 * x29) by A41, A42, A98, A97 ;
then 2 * x19 = 2 * x29 by ;
hence x1 = x2 by ; :: thesis: verum
end;
suppose A100: ( not x1 in dom g2 & x2 in dom g2 ) ; :: thesis: x1 = x2
dom h = (dom f2) \/ (dom g2) by FUNCT_4:def 1;
then A101: x1 in dom f2 by ;
then x1 in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by ;
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 ;
then A104: f . (2 * x19) in P by ;
x2 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by ;
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 ;
then A107: g . ((2 * x29) - 1) in Q by ;
A108: 1 in dom f by ;
A109: 0 in dom g by ;
A110: f . (2 * x19) = f2 . x1 by
.= h . x2 by
.= g2 . x2 by
.= g . ((2 * x29) - 1) by ;
then g . ((2 * x29) - 1) in P /\ Q by ;
then g . ((2 * x29) - 1) = p by ;
then A111: ((2 * x29) - 1) + 1 = 0 + 1 by ;
f . (2 * x19) in P /\ Q by ;
then f . (2 * x19) = p by ;
then (1 / 2) * (2 * x19) = (1 / 2) * 1 by ;
hence x1 = x2 by ; :: thesis: verum
end;
suppose A112: ( x1 in dom g2 & not x2 in dom g2 ) ; :: thesis: x1 = x2
dom h = (dom f2) \/ (dom g2) by FUNCT_4:def 1;
then A113: x2 in dom f2 by ;
then x2 in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by ;
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 ;
then A116: f . (2 * x29) in P by ;
x1 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by ;
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 ;
then A119: g . ((2 * x19) - 1) in Q by ;
A120: 1 in dom f by ;
A121: 0 in dom g by ;
A122: f . (2 * x29) = f2 . x2 by
.= h . x1 by
.= g2 . x1 by
.= g . ((2 * x19) - 1) by ;
then g . ((2 * x19) - 1) in P /\ Q by ;
then g . ((2 * x19) - 1) = p by ;
then A123: ((2 * x19) - 1) + 1 = 0 + 1 by ;
f . (2 * x29) in P /\ Q by ;
then f . (2 * x29) = p by ;
then (1 / 2) * (2 * x29) = (1 / 2) * 1 by ;
hence x1 = x2 by ; :: thesis: verum
end;
suppose A124: ( x1 in dom g2 & x2 in dom g2 ) ; :: thesis: x1 = x2
then x2 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by ;
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 ;
x1 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by ;
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 ;
g . ((2 * x19) - 1) = g2 . x1 by
.= h . x2 by
.= g2 . x2 by
.= g . ((2 * x29) - 1) by ;
then ((2 * x19) - 1) + 1 = ((2 * x29) - 1) + 1 by ;
hence x1 = x2 by ; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;
then A129: ( dom h = [#] I[01] & h is one-to-one ) by ;
reconsider h9 = h as Function of I[01],(T | (P \/ Q)) ;
take h9 ; :: thesis: ( 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
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in P or a in rng f2 )
assume a in P ; :: thesis: a in rng f2
then consider x being object such that
A132: x in dom f and
A133: a = f . x by ;
x in { r where r is Real : ( 0 <= r & r <= 1 ) } by ;
then consider x9 being Real such that
A134: x9 = x and
A135: ( 0 <= x9 & x9 <= 1 ) ;
reconsider x9 = x9 as Real ;
( 0 / 2 <= x9 / 2 & x9 / 2 <= 1 / 2 ) by ;
then x9 / 2 in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } ;
then A136: x9 / 2 in dom f2 by ;
a = f . (2 * (x9 / 2)) by
.= f2 . (x9 / 2) by ;
hence a in rng f2 by ; :: thesis: verum
end;
A137: P c= rng h
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in P or a in rng h )
assume a in P ; :: thesis: a in rng h
then consider x being object such that
A138: x in dom f2 and
A139: a = f2 . x by ;
now :: thesis: a in rng h
per cases ( x in [.(1 / 2),1.] or not x in [.(1 / 2),1.] ) ;
suppose A140: x in [.(1 / 2),1.] ; :: thesis: a in rng h
then x in [.0,(1 / 2).] /\ [.(1 / 2),1.] by ;
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 ;
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
.= g . ((2 * (1 / 2)) - 1) by
.= f2 . (1 / 2) by A5, A7, A42, A143 ;
hence a in rng h by ; :: thesis: verum
end;
suppose A144: not x in [.(1 / 2),1.] ; :: thesis: a in rng h
A145: x in (dom f2) \/ (dom g2) by ;
then A146: x in dom h by FUNCT_4:def 1;
h . x = f2 . x by ;
hence a in rng h by ; :: thesis: verum
end;
end;
end;
hence a in rng h ; :: thesis: verum
end;
( rng h c= (rng f2) \/ (rng g2) & (rng f2) \/ (rng g2) c= P \/ Q ) by ;
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 ;
then rng h = P \/ Q by ;
then A148: rng h = [#] (M | R) by PRE_TOPC:def 5;
( I[01] is compact & M | R is T_2 ) by ;
hence h9 is being_homeomorphism by ; :: thesis: ( h9 . 0 = f . 0 & h9 . 1 = g . 1 )
not 0 in dom g2 by ;
hence h9 . 0 = f2 . 0 by FUNCT_4:11
.= f . (2 * 0) by
.= f . 0 ;
:: thesis: h9 . 1 = g . 1
A149: 1 in dom g2 by ;
hence h9 . 1 = g2 . 1 by FUNCT_4:13
.= g . ((2 * 1) - 1) by
.= g . 1 ;
:: thesis: verum