let T be T_2 TopSpace; :: thesis:
let P, Q be Subset of T; :: thesis:
let p be Point of T; :: thesis:
let f be Function of I[01] ,(T | P); :: thesis:
let g be Function of I[01] ,(T | Q); :: thesis:
assume that
A1: P /\ Q = {p} and
A2: f is being_homeomorphism and
A3: f . 1 = p and
A4: g is being_homeomorphism and
A5: g . 0 = p ; :: thesis:
p in P /\ Q by A1, TARSKI:def 1;
then reconsider M = T as non empty TopSpace ;
reconsider P' = P, Q' = Q as non empty Subset of M by A1;
f is Function of the carrier of I[01] ,the carrier of (M | P') ;
then A6: dom f = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
P = [#] (T | P) by PRE_TOPC:def 10;
then A7: rng f = P by A2, TOPS_2:def 5;
g is Function of the carrier of I[01] ,the carrier of (M | Q') ;
then A9: dom g = [.0 ,1.] by BORSUK_1:83, FUNCT_2:def 1;
Q = [#] (T | Q) by PRE_TOPC:def 10;
then A10: rng g = Q by A4, TOPS_2:def 5;
A11: f is one-to-one by A2, TOPS_2:def 5;
A12: g is one-to-one by A4, TOPS_2:def 5;
defpred S₁[ set , set ] means for a being Real st a = $1 holds
$2 = f . (2 * a);
A13: for x being set st x in [.0 ,(1 / 2).] holds
ex u being set st S₁[x,u]

proof

let x be set ; :: thesis:
assume x in [.0 ,(1 / 2).] ; :: thesis:
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
A14: r = x and
( 0 <= r & r <= 1 / 2 ) ;
take f . (2 * r) ; :: thesis:
thus S₁[x,f . (2 * r)] by A14; :: thesis:

end;

consider f2 being Function such that
A15: dom f2 = [.0 ,(1 / 2).] and
A16: for x being set st x in [.0 ,(1 / 2).] holds
S₁[x,f2 . x] from CLASSES1:sch 1(A13);
defpred S₂[ set , set ] means for a being Real st a = $1 holds
$2 = g . ((2 * a) - 1);
A17: for x being set st x in [.(1 / 2),1.] holds
ex u being set st S₂[x,u]

proof

let x be set ; :: thesis:
assume x in [.(1 / 2),1.] ; :: thesis:
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
A18: r = x and
( 1 / 2 <= r & r <= 1 ) ;
take g . ((2 * r) - 1) ; :: thesis:
thus S₂[x,g . ((2 * r) - 1)] by A18; :: thesis:

end;

consider g2 being Function such that
A19: dom g2 = [.(1 / 2),1.] and
A20: for x being set st x in [.(1 / 2),1.] holds
S₂[x,g2 . x] from CLASSES1:sch 1(A17);
reconsider R = P' \/ Q' as non empty Subset of M ;
A21: R = [#] (M | R) by PRE_TOPC:def 10
.= the carrier of (M | R) ;

now

let y be set ; :: thesis:
assume y in rng f2 ; :: thesis:
then consider x being set such that
A22: ( x in dom f2 & y = f2 . x ) by FUNCT_1:def 5;
x in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by A15, A22, RCOMP_1:def 1;
then consider a being Real such that
A23: ( x = a & 0 <= a & a <= 1 / 2 ) ;
A24: y = f . (2 * a) by A15, A16, A22, A23;
( 0 <= 2 * a & 2 * a <= 2 * (1 / 2) & 0 <> 2 ) by A23, XREAL_1:66, XREAL_1:129;
then 2 * a in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then 2 * a in dom f by A6, RCOMP_1:def 1;
hence y in P by A7, A24, FUNCT_1:def 5; :: thesis:

end;

then A25: rng f2 c= P by TARSKI:def 3;

now

let y be set ; :: thesis:
assume y in rng g2 ; :: thesis:
then consider x being set such that
A26: ( x in dom g2 & y = g2 . x ) by FUNCT_1:def 5;
x in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by A19, A26, RCOMP_1:def 1;
then consider a being Real such that
A27: ( x = a & 1 / 2 <= a & a <= 1 ) ;
A28: y = g . ((2 * a) - 1) by A19, A20, A26, A27;
( 2 * (1 / 2) = 1 & 0 <= 2 ) ;
then ( 1 <= 2 * a & 2 * a <= 2 * 1 ) by A27, XREAL_1:66;
then ( 1 - 1 <= (2 * a) - 1 & (2 * a) - 1 <= (1 + 1) - 1 ) by XREAL_1:11;
then (2 * a) - 1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then (2 * a) - 1 in dom g by A9, RCOMP_1:def 1;
hence y in Q by A10, A28, FUNCT_1:def 5; :: thesis:

end;

then A29: rng g2 c= Q by TARSKI:def 3;
( 0 in [.0 ,1.] & 1 in [.0 ,1.] & 1 / 2 in [.0 ,1.] ) by XXREAL_1:1;
then ( [.0 ,(1 / 2).] c= the carrier of I[01] & [.(1 / 2),1.] c= the carrier of I[01] ) by BORSUK_1:83, XXREAL_2:def 12;
then ( the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) c= the carrier of I[01] & the carrier of (Closed-Interval-TSpace (1 / 2),1) c= the carrier of I[01] ) by TOPMETR:25;
then reconsider T1 = Closed-Interval-TSpace 0 ,(1 / 2), T2 = Closed-Interval-TSpace (1 / 2),1 as SubSpace of I[01] by TOPMETR:4;
( P c= P \/ Q & Q c= P \/ Q ) by XBOOLE_1:7;
then A30: ( dom f2 = the carrier of T1 & rng f2 c= the carrier of (T | (P \/ Q)) & dom g2 = the carrier of T2 & rng g2 c= the carrier of (M | R) ) by A15, A19, A21, A25, A29, TOPMETR:25, XBOOLE_1:1;
then reconsider f1 = f2 as Function of T1,(M | R) by FUNCT_2:def 1, RELSET_1:11;
reconsider g1 = g2 as Function of T2,(M | R) by A30, FUNCT_2:def 1, RELSET_1:11;
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:83, RCOMP_1:def 1;
A31: ( [#] T1 = [.0 ,(1 / 2).] & [#] T2 = [.(1 / 2),1.] ) by TOPMETR:25;
then ([#] T1) \/ ([#] T2) = the carrier of I[01] by BORSUK_1:83, XXREAL_1:165;
then A32: ([#] T1) \/ ([#] T2) = [#] I[01] ;
A33: ([#] T1) /\ ([#] T2) = {pp} by A31, XXREAL_1:418;
A34: ( T1 is compact & T2 is compact ) by HEINE:11;
TopSpaceMetr RealSpace is T_2 by PCOMPS_1:38;
then A35: I[01] is T_2 by TOPMETR:3, TOPMETR:def 7;
deffunc H₁( Element of REAL ) -> Element of REAL = 2 * $1;
consider f3 being Function of REAL ,REAL such that
A36: for x being Real holds f3 . x = H₁(x) from FUNCT_2:sch 4();
reconsider f3 = f3 as Function of R^1 ,R^1 by TOPMETR:24;
for x being Real holds f3 . x = (2 * x) + 0 by A36;
then A37: f3 is continuous by TOPMETR:28;
reconsider PP = [.0 ,(1 / 2).] as Subset of R^1 by TOPMETR:24;
reconsider PP = PP as non empty Subset of R^1 by XXREAL_1:1;
A38: R^1 | PP = T1 by TOPMETR:26;
A39: dom (f3 | [.0 ,(1 / 2).]) = (dom f3) /\ [.0 ,(1 / 2).] by RELAT_1:90
.= REAL /\ [.0 ,(1 / 2).] by FUNCT_2:def 1
.= [.0 ,(1 / 2).] by XBOOLE_1:28
.= the carrier of T1 by TOPMETR:25 ;
rng (f3 | [.0 ,(1 / 2).]) c= the carrier of R^1 ;
then reconsider f3' = f3 | PP as Function of T1,R^1 by A39, FUNCT_2:def 1, RELSET_1:11;
A40: f3' is continuous by A37, A38, TOPMETR:10;
A41: dom f3' = the carrier of T1 by FUNCT_2:def 1;
rng f3' c= the carrier of I[01]

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng f3' ; :: thesis:
then consider x being set such that
A42: ( x in dom f3' & y = f3' . x ) by FUNCT_1:def 5;
x in [.0 ,(1 / 2).] by A41, A42, TOPMETR:25;
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
A43: ( x = r & 0 <= r & r <= 1 / 2 ) ;
A44: y = f3 . x by A42, FUNCT_1:70
.= 2 * r by A36, A43 ;
( 2 * 0 <= 2 * r & 2 * r <= 2 * (1 / 2) & 0 <> 2 ) by A43, XREAL_1:66;
then y in { rr where rr is Real : ( 0 <= rr & rr <= 1 ) } by A44;
hence y in the carrier of I[01] by BORSUK_1:83, RCOMP_1:def 1; :: thesis:

end;

then reconsider f4 = f3' as Function of T1,I[01] by A41, RELSET_1:11;
A45: f4 is continuous by A40, PRE_TOPC:57;
A46: f is continuous by A2, TOPS_2:def 5;
( dom f = the carrier of I[01] & rng f c= the carrier of (M | R) ) by A7, A21, FUNCT_2:def 1, XBOOLE_1:7;
then reconsider ff = f as Function of I[01] ,(M | R) by RELSET_1:11;
M | P' is SubSpace of M | R by TOPMETR:5;
then A47: ff is continuous by A46, PRE_TOPC:56;
for x being set st x in the carrier of T1 holds
f1 . x = (ff * f4) . x

proof

let x be set ; :: thesis:
assume A48: x in the carrier of T1 ; :: thesis:
( the carrier of T1 = [.0 ,(1 / 2).] & [.0 ,(1 / 2).] c= REAL ) by TOPMETR:25;
then reconsider x' = x as Real by A48;
the carrier of T1 = [.0 ,(1 / 2).] by TOPMETR:25;
hence f1 . x = f . (2 * x') by A16, A48
.= f . (f3 . x') by A36
.= f . (f4 . x) by A39, A48, FUNCT_1:70
.= (ff * f4) . x by A48, FUNCT_2:21 ;
:: thesis:

end;

then f1 = ff * f4 by FUNCT_2:18;
then A49: f1 is continuous by A45, A47;
deffunc H₂( Element of REAL ) -> Element of REAL = (2 * $1) - 1;
consider g3 being Function of REAL ,REAL such that
A50: for x being Real holds g3 . x = H₂(x) from FUNCT_2:sch 4();
reconsider g3 = g3 as Function of R^1 ,R^1 by TOPMETR:24;
for x being Real holds g3 . x = (2 * x) + (- 1)

proof

let x be Real; :: thesis:
thus g3 . x = (2 * x) - 1 by A50
.= (2 * x) + (- 1) ; :: thesis:

end;

then A51: g3 is continuous by TOPMETR:28;
reconsider PP = [.(1 / 2),1.] as Subset of R^1 by TOPMETR:24;
reconsider PP = PP as non empty Subset of R^1 by XXREAL_1:1;
A52: R^1 | PP = T2 by TOPMETR:26;
A53: dom (g3 | [.(1 / 2),1.]) = (dom g3) /\ [.(1 / 2),1.] by RELAT_1:90
.= REAL /\ [.(1 / 2),1.] by FUNCT_2:def 1
.= [.(1 / 2),1.] by XBOOLE_1:28
.= the carrier of T2 by TOPMETR:25 ;
rng (g3 | [.(1 / 2),1.]) c= the carrier of R^1 ;
then reconsider g3' = g3 | PP as Function of T2,R^1 by A53, FUNCT_2:def 1, RELSET_1:11;
A54: g3' is continuous by A51, A52, TOPMETR:10;
A55: dom g3' = the carrier of T2 by FUNCT_2:def 1;
rng g3' c= the carrier of I[01]

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng g3' ; :: thesis:
then consider x being set such that
A56: ( x in dom g3' & y = g3' . x ) by FUNCT_1:def 5;
x in [.(1 / 2),1.] by A55, A56, TOPMETR:25;
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: ( x = r & 1 / 2 <= r & r <= 1 ) ;
A58: y = g3 . x by A56, FUNCT_1:70
.= (2 * r) - 1 by A50, A57 ;
( 2 * (1 / 2) <= 2 * r & 2 * r <= 2 * 1 & 0 <> 2 ) by A57, XREAL_1:66;
then ( 1 - 1 <= (2 * r) - 1 & (2 * r) - 1 <= (1 + 1) - 1 ) by XREAL_1:11;
then y in { rr where rr is Real : ( 0 <= rr & rr <= 1 ) } by A58;
hence y in the carrier of I[01] by BORSUK_1:83, RCOMP_1:def 1; :: thesis:

end;

then reconsider g4 = g3' as Function of T2,I[01] by A55, RELSET_1:11;
A59: g4 is continuous by A54, PRE_TOPC:57;
A60: g is continuous by A4, TOPS_2:def 5;
( dom g = the carrier of I[01] & rng g c= the carrier of (M | R) ) by A10, A21, FUNCT_2:def 1, XBOOLE_1:7;
then reconsider g' = g as Function of I[01] ,(M | R) by RELSET_1:11;
M | Q' is SubSpace of M | R by TOPMETR:5;
then A61: g' is continuous by A60, PRE_TOPC:56;
for x being set st x in the carrier of T2 holds
g1 . x = (g' * g4) . x

proof

let x be set ; :: thesis:
assume A62: x in the carrier of T2 ; :: thesis:
( the carrier of T2 = [.(1 / 2),1.] & [.(1 / 2),1.] c= REAL ) by TOPMETR:25;
then reconsider x' = x as Real by A62;
the carrier of T2 = [.(1 / 2),1.] by TOPMETR:25;
hence g1 . x = g . ((2 * x') - 1) by A20, A62
.= g . (g3 . x') by A50
.= g . (g4 . x) by A53, A62, FUNCT_1:70
.= (g' * g4) . x by A62, FUNCT_2:21 ;
:: thesis:

end;

then g1 = g' * g4 by FUNCT_2:18;
then A63: g1 is continuous by A59, A61;
A64: ( 1 / 2 in [.(1 / 2),1.] & 1 / 2 in [.0 ,(1 / 2).] ) by XXREAL_1:1;
then f1 . pp = g . ((2 * (1 / 2)) - 1) by A3, A5, A16
.= g1 . pp by A20, A64 ;
then reconsider h = f2 +* g2 as continuous Function of I[01] ,(M | R) by A32, A33, A34, A35, A49, A63, COMPTS_1:29;
A65: dom h = [.0 ,(1 / 2).] \/ [.(1 / 2),1.] by A15, A19, FUNCT_4:def 1
.= [.0 ,1.] by XXREAL_1:165 ;
A66: rng h c= (rng f2) \/ (rng g2) by FUNCT_4:18;
(rng f2) \/ (rng g2) c= P \/ Q by A25, A29, XBOOLE_1:13;
then A67: rng h c= P \/ Q by A66, XBOOLE_1:1;
reconsider h' = h as Function of I[01] ,(T | (P \/ Q)) ;
take h' ; :: thesis:
A68: I[01] is compact by HEINE:11, TOPMETR:27;
A69: M | R is T_2 by TOPMETR:3;
A70: rng g2 c= rng h by FUNCT_4:19;
Q c= rng g2

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in Q ; :: thesis:
then consider x being set such that
A71: ( x in dom g & a = g . x ) by A10, FUNCT_1:def 5;
x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A9, A71, RCOMP_1:def 1;
then consider x' being Real such that
A72: ( x' = x & 0 <= x' & x' <= 1 ) ;
( 0 + 1 <= x' + 1 & x' + 1 <= 1 + 1 & 2 <> 0 & 2 > 0 ) by A72, XREAL_1:8;
then ( 1 / 2 <= (x' + 1) / 2 & (x' + 1) / 2 <= 2 / 2 & 2 <> 0 ) by XREAL_1:74;
then (x' + 1) / 2 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ;
then A73: (x' + 1) / 2 in dom g2 by A19, RCOMP_1:def 1;
a = g . ((2 * ((x' + 1) / 2)) - 1) by A71, A72
.= g2 . ((x' + 1) / 2) by A19, A20, A73 ;
hence a in rng g2 by A73, FUNCT_1:def 5; :: thesis:

end;

then A74: Q c= rng h by A70, XBOOLE_1:1;
A75: P c= rng f2

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in P ; :: thesis:
then consider x being set such that
A76: ( x in dom f & a = f . x ) by A7, FUNCT_1:def 5;
x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A6, A76, RCOMP_1:def 1;
then consider x' being Real such that
A77: ( x' = x & 0 <= x' & x' <= 1 ) ;
( 0 / 2 <= x' / 2 & x' / 2 <= 1 / 2 & 2 <> 0 ) by A77, XREAL_1:74;
then x' / 2 in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } ;
then A78: x' / 2 in dom f2 by A15, RCOMP_1:def 1;
a = f . (2 * (x' / 2)) by A76, A77
.= f2 . (x' / 2) by A15, A16, A78 ;
hence a in rng f2 by A78, FUNCT_1:def 5; :: thesis:

end;

P c= rng h

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in P ; :: thesis:
then consider x being set such that
A79: ( x in dom f2 & a = f2 . x ) by A75, FUNCT_1:def 5;

now

per cases ;

suppose A80: x in [.(1 / 2),1.] ; :: thesis:

then x in [.0 ,(1 / 2).] /\ [.(1 / 2),1.] by A15, A79, XBOOLE_0:def 4;
then x in {(1 / 2)} by XXREAL_1:418;
then A81: x = 1 / 2 by TARSKI:def 1;
A82: 1 / 2 in [.0 ,(1 / 2).] by XXREAL_1:1;
A83: h . x = g2 . x by A19, A80, FUNCT_4:14
.= g . ((2 * (1 / 2)) - 1) by A20, A80, A81
.= f2 . (1 / 2) by A3, A5, A16, A82 ;
x in (dom f2) \/ (dom g2) by A79, XBOOLE_0:def 3;
then x in dom h by FUNCT_4:def 1;
hence a in rng h by A79, A81, A83, FUNCT_1:def 5; :: thesis:

end;

suppose A84: not x in [.(1 / 2),1.] ; :: thesis:

A85: x in (dom f2) \/ (dom g2) by A79, XBOOLE_0:def 3;
then A86: x in dom h by FUNCT_4:def 1;
h . x = f2 . x by A19, A84, A85, FUNCT_4:def 1;
hence a in rng h by A79, A86, FUNCT_1:def 5; :: thesis:

end;

hence a in rng h ; :: thesis:

end;

then P \/ Q c= rng h by A74, XBOOLE_1:8;
then rng h = P \/ Q by A67, XBOOLE_0:def 10;
then A87: rng h = [#] (M | R) by PRE_TOPC:def 10;
dom h = the carrier of I[01] by FUNCT_2:def 1;
then A88: dom h = [#] I[01] ;

A89: now

let x be Real; :: thesis:
assume x in dom f2 ; :: thesis:
then x in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by A15, RCOMP_1:def 1;
then consider a being Real such that
A90: ( a = x & 0 <= a & a <= 1 / 2 ) ;
( 0 <= 2 * a & 2 * a <= 2 * (1 / 2) & 0 <> 2 ) by A90, XREAL_1:66, XREAL_1:129;
then 2 * a in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
hence 2 * x in dom f by A6, A90, RCOMP_1:def 1; :: thesis:

end;

A91: now

let x be Real; :: thesis:
assume x in dom g2 ; :: thesis:
then x in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by A19, RCOMP_1:def 1;
then consider a being Real such that
A92: ( a = x & 1 / 2 <= a & a <= 1 ) ;
( 2 * (1 / 2) = 1 & 0 <= 2 ) ;
then ( 1 <= 2 * a & 2 * a <= 2 * 1 ) by A92, XREAL_1:66;
then ( 1 - 1 <= (2 * a) - 1 & (2 * a) - 1 <= (1 + 1) - 1 ) by XREAL_1:11;
then (2 * a) - 1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
hence (2 * x) - 1 in dom g by A9, A92, RCOMP_1:def 1; :: thesis:

end;

now

let x1, x2 be set ; :: thesis:
assume that
A93: ( x1 in dom h & x2 in dom h ) and
A94: h . x1 = h . x2 ; :: thesis:

now

per cases ;

suppose A95: ( not x1 in dom g2 & not x2 in dom g2 ) ; :: thesis:

A96: dom h = (dom f2) \/ (dom g2) by FUNCT_4:def 1;
then A97: ( x1 in dom f2 & x2 in dom f2 ) by A93, A95, XBOOLE_0:def 3;
A98: ( x1 in [.0 ,(1 / 2).] & x2 in [.0 ,(1 / 2).] ) by A15, A93, A95, A96, XBOOLE_0:def 3;
then x1 in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by RCOMP_1:def 1;
then consider x1' being Real such that
A99: x1' = x1 and
( 0 <= x1' & x1' <= 1 / 2 ) ;
x2 in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by A98, RCOMP_1:def 1;
then consider x2' being Real such that
A100: x2' = x2 and
( 0 <= x2' & x2' <= 1 / 2 ) ;
A101: ( 2 * x1' in dom f & 2 * x2' in dom f ) by A89, A97, A99, A100;
f . (2 * x1') = f2 . x1 by A15, A16, A97, A99
.= h . x2 by A94, A95, FUNCT_4:12
.= f2 . x2 by A95, FUNCT_4:12
.= f . (2 * x2') by A15, A16, A97, A100 ;
then ( 2 * x1' = 2 * x2' & 2 <> 0 ) by A11, A101, FUNCT_1:def 8;
hence x1 = x2 by A99, A100; :: thesis:

end;

suppose A102: ( not x1 in dom g2 & x2 in dom g2 ) ; :: thesis:

then x2 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by A19, RCOMP_1:def 1;
then consider x2' being Real such that
A103: x2' = x2 and
( 1 / 2 <= x2' & x2' <= 1 ) ;
dom h = (dom f2) \/ (dom g2) by FUNCT_4:def 1;
then A104: x1 in dom f2 by A93, A102, XBOOLE_0:def 3;
then x1 in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by A15, RCOMP_1:def 1;
then consider x1' being Real such that
A105: x1' = x1 and
( 0 <= x1' & x1' <= 1 / 2 ) ;
A106: f . (2 * x1') = f2 . x1 by A15, A16, A104, A105
.= h . x2 by A94, A102, FUNCT_4:12
.= g2 . x2 by A102, FUNCT_4:14
.= g . ((2 * x2') - 1) by A19, A20, A102, A103 ;
A107: ( 2 * x1' in dom f & (2 * x2') - 1 in dom g ) by A89, A91, A102, A103, A104, A105;
then ( f . (2 * x1') in P & g . ((2 * x2') - 1) in Q ) by A7, A10, FUNCT_1:def 5;
then ( f . (2 * x1') in P /\ Q & g . ((2 * x2') - 1) in P /\ Q ) by A106, XBOOLE_0:def 4;
then A108: ( f . (2 * x1') = p & g . ((2 * x2') - 1) = p ) by A1, TARSKI:def 1;
( 0 in dom g & 1 in dom f ) by A6, A9, XXREAL_1:1;
then ( (1 / 2) * (2 * x1') = (1 / 2) * 1 & ((2 * x2') - 1) + 1 = 0 + 1 ) by A3, A5, A11, A12, A107, A108, FUNCT_1:def 8;
hence x1 = x2 by A103, A105; :: thesis:

end;

suppose A109: ( x1 in dom g2 & not x2 in dom g2 ) ; :: thesis:

then x1 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by A19, RCOMP_1:def 1;
then consider x1' being Real such that
A110: x1' = x1 and
( 1 / 2 <= x1' & x1' <= 1 ) ;
dom h = (dom f2) \/ (dom g2) by FUNCT_4:def 1;
then A111: x2 in dom f2 by A93, A109, XBOOLE_0:def 3;
then x2 in { a where a is Real : ( 0 <= a & a <= 1 / 2 ) } by A15, RCOMP_1:def 1;
then consider x2' being Real such that
A112: x2' = x2 and
( 0 <= x2' & x2' <= 1 / 2 ) ;
A113: f . (2 * x2') = f2 . x2 by A15, A16, A111, A112
.= h . x1 by A94, A109, FUNCT_4:12
.= g2 . x1 by A109, FUNCT_4:14
.= g . ((2 * x1') - 1) by A19, A20, A109, A110 ;
A114: ( 2 * x2' in dom f & (2 * x1') - 1 in dom g ) by A89, A91, A109, A110, A111, A112;
then ( f . (2 * x2') in P & g . ((2 * x1') - 1) in Q ) by A7, A10, FUNCT_1:def 5;
then ( f . (2 * x2') in P /\ Q & g . ((2 * x1') - 1) in P /\ Q ) by A113, XBOOLE_0:def 4;
then A115: ( f . (2 * x2') = p & g . ((2 * x1') - 1) = p ) by A1, TARSKI:def 1;
( 0 in dom g & 1 in dom f ) by A6, A9, XXREAL_1:1;
then ( (1 / 2) * (2 * x2') = (1 / 2) * 1 & ((2 * x1') - 1) + 1 = 0 + 1 ) by A3, A5, A11, A12, A114, A115, FUNCT_1:def 8;
hence x1 = x2 by A110, A112; :: thesis:

end;

suppose A116: ( x1 in dom g2 & x2 in dom g2 ) ; :: thesis:

then x1 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by A19, RCOMP_1:def 1;
then consider x1' being Real such that
A117: x1' = x1 and
( 1 / 2 <= x1' & x1' <= 1 ) ;
x2 in { a where a is Real : ( 1 / 2 <= a & a <= 1 ) } by A19, A116, RCOMP_1:def 1;
then consider x2' being Real such that
A118: x2' = x2 and
( 1 / 2 <= x2' & x2' <= 1 ) ;
A119: ( (2 * x1') - 1 in dom g & (2 * x2') - 1 in dom g ) by A91, A116, A117, A118;
g . ((2 * x1') - 1) = g2 . x1 by A19, A20, A116, A117
.= h . x2 by A94, A116, FUNCT_4:14
.= g2 . x2 by A116, FUNCT_4:14
.= g . ((2 * x2') - 1) by A19, A20, A116, A118 ;
then ((2 * x1') - 1) + 1 = ((2 * x2') - 1) + 1 by A12, A119, FUNCT_1:def 8;
hence x1 = x2 by A117, A118; :: thesis:

end;

hence x1 = x2 ; :: thesis:

end;

then h is one-to-one by FUNCT_1:def 8;
hence h' is being_homeomorphism by A68, A69, A87, A88, COMPTS_1:26; :: thesis:
A120: 0 in [.0 ,(1 / 2).] by XXREAL_1:1;
( 0 in dom h & not 0 in dom g2 ) by A19, A65, XXREAL_1:1;
hence h' . 0 = f2 . 0 by FUNCT_4:12
.= f . (2 * 0 ) by A16, A120
.= f . 0 ;
:: thesis:
A121: 1 in dom g2 by A19, XXREAL_1:1;
hence h' . 1 = g2 . 1 by FUNCT_4:14
.= g . ((2 * 1) - 1) by A19, A20, A121
.= g . 1 ;
:: thesis: