:: TOPMETR2 semantic presentation begin theorem :: TOPMETR2:1 for f, g being Function st f is one-to-one & g is one-to-one & ( for x1, x2 being set st x1 in dom g & x2 in (dom f) \ (dom g) holds g . x1 <> f . x2 ) holds f +* g is one-to-one proof let f, g be Function; ::_thesis: ( f is one-to-one & g is one-to-one & ( for x1, x2 being set st x1 in dom g & x2 in (dom f) \ (dom g) holds g . x1 <> f . x2 ) implies f +* g is one-to-one ) assume that A1: f is one-to-one and A2: g is one-to-one and A3: for x1, x2 being set st x1 in dom g & x2 in (dom f) \ (dom g) holds g . x1 <> f . x2 ; ::_thesis: f +* g is one-to-one now__::_thesis:_for_x11,_x22_being_set_st_x11_in_dom_(f_+*_g)_&_x22_in_dom_(f_+*_g)_&_(f_+*_g)_._x11_=_(f_+*_g)_._x22_holds_ x11_=_x22 let x11, x22 be set ; ::_thesis: ( x11 in dom (f +* g) & x22 in dom (f +* g) & (f +* g) . x11 = (f +* g) . x22 implies x11 = x22 ) assume that A4: x11 in dom (f +* g) and A5: x22 in dom (f +* g) and A6: (f +* g) . x11 = (f +* g) . x22 ; ::_thesis: x11 = x22 A7: x22 in (dom f) \/ (dom g) by A5, FUNCT_4:def_1; then A8: x22 in ((dom f) \ (dom g)) \/ (dom g) by XBOOLE_1:39; A9: x11 in (dom f) \/ (dom g) by A4, FUNCT_4:def_1; then A10: x11 in ((dom f) \ (dom g)) \/ (dom g) by XBOOLE_1:39; now__::_thesis:_x11_=_x22 percases ( x11 in (dom f) \ (dom g) or x11 in dom g ) by A10, XBOOLE_0:def_3; supposeA11: x11 in (dom f) \ (dom g) ; ::_thesis: x11 = x22 then not x11 in dom g by XBOOLE_0:def_5; then A12: (f +* g) . x11 = f . x11 by A9, FUNCT_4:def_1; now__::_thesis:_(_(_x22_in_(dom_f)_\_(dom_g)_&_x11_=_x22_)_or_(_x22_in_dom_g_&_contradiction_)_) percases ( x22 in (dom f) \ (dom g) or x22 in dom g ) by A8, XBOOLE_0:def_3; caseA13: x22 in (dom f) \ (dom g) ; ::_thesis: x11 = x22 then not x22 in dom g by XBOOLE_0:def_5; then f . x11 = f . x22 by A6, A7, A12, FUNCT_4:def_1; hence x11 = x22 by A1, A11, A13, FUNCT_1:def_4; ::_thesis: verum end; caseA14: x22 in dom g ; ::_thesis: contradiction then g . x22 <> f . x11 by A3, A11; hence contradiction by A6, A7, A12, A14, FUNCT_4:def_1; ::_thesis: verum end; end; end; hence x11 = x22 ; ::_thesis: verum end; supposeA15: x11 in dom g ; ::_thesis: x11 = x22 now__::_thesis:_(_(_x22_in_(dom_f)_\_(dom_g)_&_contradiction_)_or_(_x22_in_dom_g_&_x11_=_x22_)_) percases ( x22 in (dom f) \ (dom g) or x22 in dom g ) by A8, XBOOLE_0:def_3; caseA16: x22 in (dom f) \ (dom g) ; ::_thesis: contradiction then not x22 in dom g by XBOOLE_0:def_5; then A17: (f +* g) . x22 = f . x22 by A7, FUNCT_4:def_1; g . x11 <> f . x22 by A3, A15, A16; hence contradiction by A6, A9, A15, A17, FUNCT_4:def_1; ::_thesis: verum end; caseA18: x22 in dom g ; ::_thesis: x11 = x22 then (f +* g) . x22 = g . x22 by A7, FUNCT_4:def_1; then g . x11 = g . x22 by A6, A9, A15, FUNCT_4:def_1; hence x11 = x22 by A2, A15, A18, FUNCT_1:def_4; ::_thesis: verum end; end; end; hence x11 = x22 ; ::_thesis: verum end; end; end; hence x11 = x22 ; ::_thesis: verum end; hence f +* g is one-to-one by FUNCT_1:def_4; ::_thesis: verum end; Lm1: for f, g being Function st f .: ((dom f) /\ (dom g)) c= rng g holds (rng f) \ (rng g) c= rng (f +* g) proof let f, g be Function; ::_thesis: ( f .: ((dom f) /\ (dom g)) c= rng g implies (rng f) \ (rng g) c= rng (f +* g) ) assume A1: f .: ((dom f) /\ (dom g)) c= rng g ; ::_thesis: (rng f) \ (rng g) c= rng (f +* g) let y1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not y1 in (rng f) \ (rng g) or y1 in rng (f +* g) ) assume A2: y1 in (rng f) \ (rng g) ; ::_thesis: y1 in rng (f +* g) then consider x1 being set such that A3: x1 in dom f and A4: y1 = f . x1 by FUNCT_1:def_3; A5: x1 in (dom f) \/ (dom g) by A3, XBOOLE_0:def_3; then A6: x1 in dom (f +* g) by FUNCT_4:def_1; now__::_thesis:_not_x1_in_dom_g assume x1 in dom g ; ::_thesis: contradiction then x1 in (dom f) /\ (dom g) by A3, XBOOLE_0:def_4; then f . x1 in f .: ((dom f) /\ (dom g)) by A3, FUNCT_1:def_6; hence contradiction by A1, A2, A4, XBOOLE_0:def_5; ::_thesis: verum end; then (f +* g) . x1 = f . x1 by A5, FUNCT_4:def_1; hence y1 in rng (f +* g) by A4, A6, FUNCT_1:def_3; ::_thesis: verum end; theorem :: TOPMETR2:2 for f, g being Function st f .: ((dom f) /\ (dom g)) c= rng g holds (rng f) \/ (rng g) = rng (f +* g) proof let f, g be Function; ::_thesis: ( f .: ((dom f) /\ (dom g)) c= rng g implies (rng f) \/ (rng g) = rng (f +* g) ) assume f .: ((dom f) /\ (dom g)) c= rng g ; ::_thesis: (rng f) \/ (rng g) = rng (f +* g) then A1: (rng f) \ (rng g) c= rng (f +* g) by Lm1; rng g c= rng (f +* g) by FUNCT_4:18; then ((rng f) \ (rng g)) \/ (rng g) c= rng (f +* g) by A1, XBOOLE_1:8; then A2: (rng f) \/ (rng g) c= rng (f +* g) by XBOOLE_1:39; rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; hence (rng f) \/ (rng g) = rng (f +* g) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: TOPMETR2:3 for T being T_2 TopSpace for P, Q being Subset of T for p being Point of T for f being Function of I[01],(T | P) for g being Function of I[01],(T | Q) st P /\ Q = {p} & f is being_homeomorphism & f . 1 = p & g is being_homeomorphism & g . 0 = p holds ex h being Function of I[01],(T | (P \/ Q)) st ( h is being_homeomorphism & h . 0 = f . 0 & h . 1 = g . 1 ) proof 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 H1( Element of REAL ) -> Element of REAL = 2 * \$1; 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 S1[ set , set ] 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 Real holds f3 . x = H1(x) from FUNCT_2:sch_4(); A11: R = [#] (M | R) by PRE_TOPC:def_5 .= the carrier of (M | R) ; then dom g = the carrier of I[01] by FUNCT_2:def_1; then reconsider g9 = g as Function of I[01],(M | R) by A8, A11, RELSET_1:4, XBOOLE_1:7; A12: M | Q9 is SubSpace of M | R by TOPMETR:4; g is continuous by A6, TOPS_2:def_5; then A13: g9 is continuous by A12, PRE_TOPC:26; reconsider PP = PP as non empty Subset of R^1 by XXREAL_1:1; A14: ( T1 is compact & T2 is compact ) by HEINE:4; P = [#] (T | P) by PRE_TOPC:def_5; then A15: rng f = P by A4, TOPS_2:def_5; dom f = the carrier of I[01] by A11, FUNCT_2:def_1; then reconsider ff = f as Function of I[01],(M | R) by A15, A11, RELSET_1:4, XBOOLE_1:7; f is continuous by A4, TOPS_2:def_5; then A16: ff is continuous by A9, PRE_TOPC:26; reconsider f3 = f3 as Function of R^1,R^1 by TOPMETR:17; A17: dom (f3 | [.0,(1 / 2).]) = (dom f3) /\ [.0,(1 / 2).] by RELAT_1:61 .= REAL /\ [.0,(1 / 2).] by FUNCT_2:def_1 .= [.0,(1 / 2).] by XBOOLE_1:28 .= the carrier of T1 by TOPMETR:18 ; rng (f3 | [.0,(1 / 2).]) c= the carrier of R^1 ; then reconsider f39 = f3 | PP as Function of T1,R^1 by A17, FUNCT_2:def_1, RELSET_1:4; A18: dom f39 = the carrier of T1 by FUNCT_2:def_1; rng f39 c= the carrier of I[01] proof let y be set ; :: 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 set 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; y = f3 . x by A19, A20, FUNCT_1:47 .= 2 * 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 = (2 * x) + 0 by A10; then f39 is continuous by A24, TOPMETR:7, TOPMETR:21; then A25: f4 is continuous by PRE_TOPC:27; reconsider PP = [.(1 / 2),1.] as Subset of R^1 by TOPMETR:17; reconsider PP = PP as non empty Subset of R^1 by XXREAL_1:1; deffunc H2( Element of REAL ) -> Element of REAL = (2 * \$1) - 1; consider g3 being Function of REAL,REAL such that A26: for x being Real holds g3 . x = H2(x) from FUNCT_2:sch_4(); reconsider g3 = g3 as Function of R^1,R^1 by TOPMETR:17; A27: dom (g3 | [.(1 / 2),1.]) = (dom g3) /\ [.(1 / 2),1.] by RELAT_1:61 .= REAL /\ [.(1 / 2),1.] by FUNCT_2:def_1 .= [.(1 / 2),1.] by XBOOLE_1:28 .= the carrier of T2 by TOPMETR:18 ; rng (g3 | [.(1 / 2),1.]) c= the carrier of R^1 ; then reconsider g39 = g3 | PP as Function of T2,R^1 by A27, FUNCT_2:def_1, RELSET_1:4; A28: dom g39 = the carrier of T2 by FUNCT_2:def_1; rng g39 c= the carrier of I[01] proof let y be set ; :: 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 set 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; y = g3 . x by A29, A30, FUNCT_1:47 .= (2 * r) - 1 by A26, A31 ; 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) thus g3 . x = (2 * x) - 1 by A26 .= (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 set st x in [.0,(1 / 2).] holds ex u being set st S1[x,u] proof let x be set ; ::_thesis: ( x in [.0,(1 / 2).] implies ex u being set st S1[x,u] ) assume x in [.0,(1 / 2).] ; ::_thesis: ex u being set 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 set st x in [.0,(1 / 2).] holds S1[x,f2 . x] from CLASSES1:sch_1(A39); A43: dom f2 = the carrier of T1 by A41, TOPMETR:18; f is Function of the carrier of I[01], the carrier of (M | P9) ; then A44: dom f = [.0,1.] by BORSUK_1:40, FUNCT_2:def_1; now__::_thesis:_for_y_being_set_st_y_in_rng_f2_holds_ y_in_P let y be set ; ::_thesis: ( y in rng f2 implies y in P ) assume y in rng f2 ; ::_thesis: y in P then consider x being set 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 by TARSKI:def_3; P c= P \/ Q by XBOOLE_1:7; then rng f2 c= the carrier of (T | (P \/ Q)) by A11, A50, XBOOLE_1:1; then reconsider f1 = f2 as Function of T1,(M | R) by A43, FUNCT_2:def_1, RELSET_1:4; for x being set st x in the carrier of T1 holds f1 . x = (ff * f4) . x proof let x be set ; ::_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 Real by A51; the carrier of T1 = [.0,(1 / 2).] by TOPMETR:18; hence f1 . x = f . (2 * x9) by A42, A51 .= 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 S2[ set , set ] means for a being Real st a = \$1 holds \$2 = g . ((2 * a) - 1); A56: for x being set st x in [.(1 / 2),1.] holds ex u being set st S2[x,u] proof let x be set ; ::_thesis: ( x in [.(1 / 2),1.] implies ex u being set st S2[x,u] ) assume x in [.(1 / 2),1.] ; ::_thesis: ex u being set 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 set st x in [.(1 / 2),1.] holds S2[x,g2 . x] from CLASSES1:sch_1(A56); A60: dom g2 = the carrier of T2 by A58, TOPMETR:18; g is Function of the carrier of I[01], the carrier of (M | Q9) ; then A61: dom g = [.0,1.] by BORSUK_1:40, FUNCT_2:def_1; now__::_thesis:_for_y_being_set_st_y_in_rng_g2_holds_ y_in_Q let y be set ; ::_thesis: ( y in rng g2 implies y in Q ) assume y in rng g2 ; ::_thesis: y in Q then consider x being set 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 by TARSKI:def_3; A70: Q c= rng g2 proof let a be set ; :: 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 set 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, XBOOLE_1:1; then reconsider g1 = g2 as Function of T2,(M | R) by A60, FUNCT_2:def_1, RELSET_1:4; for x being set st x in the carrier of T2 holds g1 . x = (g9 * g4) . x proof let x be set ; ::_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 Real by A85; the carrier of T2 = [.(1 / 2),1.] by TOPMETR:18; hence g1 . x = g . ((2 * x9) - 1) by A59, A85 .= 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_set_st_x1_in_dom_h_&_x2_in_dom_h_&_h_._x1_=_h_._x2_holds_ x1_=_x2 let x1, x2 be set ; ::_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 percases ( ( 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 ) ) ; supposeA92: ( 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 ; 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 ; 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; supposeA100: ( 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 ; 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 ; 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; supposeA112: ( 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 ; 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 ; 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; supposeA124: ( 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 ; 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 ; 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 set ; :: 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 set 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 ) ; ( 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 set ; :: 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 set such that A138: x in dom f2 and A139: a = f2 . x by A131, FUNCT_1:def_3; now__::_thesis:_a_in_rng_h percases ( x in [.(1 / 2),1.] or not x in [.(1 / 2),1.] ) ; supposeA140: 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; supposeA144: 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 by XBOOLE_1:1; rng g2 c= rng h by FUNCT_4:18; then Q c= rng h by A70, XBOOLE_1:1; 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 end;