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 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 H₁( 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 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 S₁[ 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 = H₁(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]

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 A18, A19, TOPMETR:18;
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 A22, XREAL_1:64;
reconsider r = r as Element of REAL by XREAL_0:def 1;
y = f3 . x by A19, A20, FUNCT_1:47
.= H₁(r) by A10, A21 ;
then y in { rr where rr is Real : ( 0 <= rr & rr <= 1 ) } by A23;
hence y in the carrier of I[01] by BORSUK_1:40, RCOMP_1:def 1; :: thesis: verum

end;

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

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 = H₁(x) + 0 by A10;
hence f3 . x = (dwa * x) + 0 ; :: thesis: verum

end;

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 H₂( 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 = H₂(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 ; :: 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 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
.= H₂(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; :: thesis: 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)

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 = H₂(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 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 S₁[x,u]

proof

let x be object ; :: thesis: ( x in [.0,(1 / 2).] implies ex u being object st S₁[x,u] )
assume x in [.0,(1 / 2).] ; :: thesis: ex u being object st S₁[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: S₁[x,f . (2 * r)]
thus S₁[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
S₁[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 :: 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 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; :: 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 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

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 A42, A51
.= f . H₁(x9)
.= f . (f3 . x9) by A10
.= f . (f4 . x) by A17, A51, FUNCT_1:47
.= (ff * f4) . x by A51, FUNCT_2:15 ;
:: thesis: verum

end;

then A52: f1 is continuous by A25, A16, FUNCT_2:12;

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 A41, RCOMP_1:def 1;
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 A55, XREAL_1:64, XREAL_1:127;
then 2 * a in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
hence 2 * x in dom f by A44, A54, RCOMP_1:def 1; :: thesis: verum

end;

defpred S₂[ 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 S₂[x,u]

proof

let x be object ; :: thesis: ( x in [.(1 / 2),1.] implies ex u being object st S₂[x,u] )
assume x in [.(1 / 2),1.] ; :: thesis: ex u being object st S₂[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: S₂[x,g . ((2 * r) - 1)]
thus S₂[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
S₂[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 :: 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 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; :: 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 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; :: thesis: 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;

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 A58, RCOMP_1:def 1;
then consider a being Real such that
A81: a = x and
A82: 1 / 2 <= a and
A83: a <= 1 ;
2 * a <= 2 * 1 by A83, XREAL_1:64;
then A84: (2 * a) - 1 <= (1 + 1) - 1 by XREAL_1:9;
2 * (1 / 2) = 1 ;
then 1 <= 2 * a by A82, 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 A84;
hence (2 * x) - 1 in dom g by A61, A81, RCOMP_1:def 1; :: thesis: verum

end;

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

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 A59, A85
.= g . H₂(x9)
.= g . (g3 . x9) by A26
.= g . (g4 . x) by A27, A85, FUNCT_1:47
.= (g9 * g4) . x by A85, FUNCT_2:15 ;
:: thesis: verum

end;

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 :: 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 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; :: 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 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; :: 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 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; :: 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 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; :: thesis: verum

end;

end;

end;

hence x1 = x2 ; :: thesis: 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 ; :: 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 A15, FUNCT_1:def 3;
x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A44, A132, RCOMP_1:def 1;
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 A135, XREAL_1:72;
then x9 / 2 in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } ;
then A136: x9 / 2 in dom f2 by A41, RCOMP_1:def 1;
a = f . (2 * (x9 / 2)) by A133, A134
.= f2 . (x9 / 2) by A41, A42, A136 ;
hence a in rng f2 by A136, FUNCT_1:def 3; :: 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 A131, FUNCT_1:def 3;

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 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; :: thesis: verum

end;

suppose A144: not x in [.(1 / 2),1.] ; :: thesis: a in rng h

A145: x in (dom f2) \/ (dom g2) by A138, XBOOLE_0:def 3;
then A146: x in dom h by FUNCT_4:def 1;
h . x = f2 . x by A58, A144, A145, FUNCT_4:def 1;
hence a in rng h by A139, A146, FUNCT_1:def 3; :: 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 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; :: thesis: ( 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 ;
:: thesis: 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 ;
:: thesis: verum