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_{1}( 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_{1}[ 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_{1}(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]

A24: R^1 | PP = T1 by TOPMETR:19;

for x being Real holds f3 . x = (dwa * x) + 0

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_{2}( 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_{2}(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]

( [#] 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)

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_{1}[x,u]

A41: dom f2 = [.0,(1 / 2).] and

A42: for x being object st x in [.0,(1 / 2).] holds

S_{1}[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;

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

_{2}[ 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_{2}[x,u]

A58: dom g2 = [.(1 / 2),1.] and

A59: for x being object st x in [.(1 / 2),1.] holds

S_{2}[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;

A70: Q c= rng g2

then A78: I[01] is T_2 by TOPMETR:2, TOPMETR:def 6;

A79: 1 / 2 in [.(1 / 2),1.] by XXREAL_1:1;

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

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;

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

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

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

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

$2 = f . (2 * a);

consider f3 being Function of REAL,REAL such that

A10: for x being Element of REAL holds f3 . x = H

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

then reconsider f4 = f39 as Function of T1,I[01] by A18, RELSET_1:4;
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_{1}(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;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

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

A24: R^1 | PP = T1 by TOPMETR:19;

for x being Real holds f3 . x = (dwa * x) + 0

proof

then
f39 is continuous
by A24, TOPMETR:7, TOPMETR:21;
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_{1}(x) + 0
by A10;

hence f3 . x = (dwa * x) + 0 ; :: thesis: verum

end;reconsider x = x as Element of REAL by XREAL_0:def 1;

f3 . x = H

hence f3 . x = (dwa * x) + 0 ; :: thesis: verum

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

consider g3 being Function of REAL,REAL such that

A26: for x being Element of REAL holds g3 . x = H

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

then reconsider g4 = g39 as Function of T2,I[01] by A28, RELSET_1:4;
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_{2}(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;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

.= (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

( [#] 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

R^1 | PP = T2
by TOPMETR:19;
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_{2}(x)
by A26

.= (dwa * x) - 1

.= (2 * x) + (- 1) ;

hence g3 . x = (2 * x) + (- 1) ; :: thesis: verum

end;reconsider x = x as Element of REAL by XREAL_0:def 1;

g3 . x = H

.= (dwa * x) - 1

.= (2 * x) + (- 1) ;

hence g3 . x = (2 * x) + (- 1) ; :: thesis: verum

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

proof

consider f2 being Function such that
let x be object ; :: thesis: ( x in [.0,(1 / 2).] implies ex u being object st S_{1}[x,u] )

assume x in [.0,(1 / 2).] ; :: thesis: ex u being object st S_{1}[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_{1}[x,f . (2 * r)]

thus S_{1}[x,f . (2 * r)]
by A40; :: thesis: verum

end;assume x in [.0,(1 / 2).] ; :: thesis: ex u being object st S

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

thus S

A41: dom f2 = [.0,(1 / 2).] and

A42: for x being object st x in [.0,(1 / 2).] holds

S

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

then A50:
rng f2 c= P
;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;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

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

then A52:
f1 is continuous
by A25, A16, FUNCT_2:12;
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_{1}(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;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

.= f . (f3 . x9) by A10

.= f . (f4 . x) by A17, A51, FUNCT_1:47

.= (ff * f4) . x by A51, FUNCT_2:15 ;

:: thesis: verum

A53: now :: thesis: for x being Real st x in dom f2 holds

2 * x in dom f

defpred S2 * 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;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

$2 = g . ((2 * a) - 1);

A56: for x being object st x in [.(1 / 2),1.] holds

ex u being object st S

proof

consider g2 being Function such that
let x be object ; :: thesis: ( x in [.(1 / 2),1.] implies ex u being object st S_{2}[x,u] )

assume x in [.(1 / 2),1.] ; :: thesis: ex u being object st S_{2}[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_{2}[x,g . ((2 * r) - 1)]

thus S_{2}[x,g . ((2 * r) - 1)]
by A57; :: thesis: verum

end;assume x in [.(1 / 2),1.] ; :: thesis: ex u being object st S

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

thus S

A58: dom g2 = [.(1 / 2),1.] and

A59: for x being object st x in [.(1 / 2),1.] holds

S

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

then A69:
rng g2 c= Q
;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;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

A70: Q c= rng g2

proof

TopSpaceMetr RealSpace is T_2
by PCOMPS_1:34;
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;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

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

Q c= P \/ Q
by XBOOLE_1:7;(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;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

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

then A86:
g1 is continuous
by A38, A13, FUNCT_2:12;
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_{2}(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;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

.= g . (g3 . x9) by A26

.= g . (g4 . x) by A27, A85, FUNCT_1:47

.= (g9 * g4) . x by A85, FUNCT_2:15 ;

:: thesis: verum

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

then A129:
( dom h = [#] I[01] & h is one-to-one )
by FUNCT_1:def 4, FUNCT_2:def 1;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

end;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 = x2end;

hence
x1 = x2
; :: thesis: verumper 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 ) )
;

end;

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;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

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;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

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;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

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;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

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

A137:
P c= rng h
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;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

proof

( rng h c= (rng f2) \/ (rng g2) & (rng f2) \/ (rng g2) c= P \/ Q )
by A50, A69, FUNCT_4:17, XBOOLE_1:13;
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;

end;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 hend;

hence
a in rng h
; :: thesis: verumper cases
( x in [.(1 / 2),1.] or not x in [.(1 / 2),1.] )
;

end;

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;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

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;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

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