:: Some Facts about Union of Two Functions and Continuity of Union of Functions :: by Yatsuka Nakamura and Agata Darmochwa{\l} :: :: Received November 21, 1991 :: Copyright (c) 1991-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, REAL_1, FUNCT_1, RELAT_1, XBOOLE_0, FUNCT_4, TARSKI, PRE_TOPC, SUBSET_1, BORSUK_1, TOPS_2, CARD_1, ARYTM_3, XXREAL_0, XXREAL_1, TOPMETR, STRUCT_0, ORDINAL2, RCOMP_1, ARYTM_1, PCOMPS_1, METRIC_1, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, RCOMP_1, METRIC_1, PCOMPS_1, TOPMETR, XXREAL_0; constructors FUNCT_4, REAL_1, MEMBERED, RCOMP_1, TOPS_2, COMPTS_1, TOPMETR, XXREAL_2, PCOMPS_1; registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, BORSUK_1, TOPMETR, XXREAL_2, XREAL_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI; equalities STRUCT_0; expansions TARSKI; theorems BORSUK_1, COMPTS_1, FUNCT_1, FUNCT_2, FUNCT_4, HEINE, TOPMETR, PCOMPS_1, PRE_TOPC, RCOMP_1, TARSKI, TOPS_2, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_1, XXREAL_2, RELAT_1, XREAL_0; schemes CLASSES1, FUNCT_2; begin reserve x,r,a for Real; reserve f,g for Function, x1,x2 for set; theorem f is one-to-one & g is one-to-one & (for x1,x2 st x1 in dom g & x2 in dom f \ dom g holds g.x1 <> f.x2) implies f+*g is one-to-one proof assume that A1: f is one-to-one and A2: g is one-to-one and A3: for x1,x2 st x1 in dom g & x2 in dom f \ dom g holds g.x1 <> f.x2; now let x11,x22 be object; assume that A4: x11 in dom (f+*g) and A5: x22 in dom (f+*g) and A6: (f+*g).x11 = (f+*g).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 per cases by A10,XBOOLE_0:def 3; suppose A11: x11 in (dom f \ dom g); 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 per cases by A8,XBOOLE_0:def 3; case A13: x22 in (dom f \ dom g); 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; end; case A14: x22 in dom g; then g.x22 <> f.x11 by A3,A11; hence contradiction by A6,A7,A12,A14,FUNCT_4:def 1; end; end; hence x11 = x22; end; suppose A15: x11 in dom g; now per cases by A8,XBOOLE_0:def 3; case A16: x22 in (dom f \ dom g); 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; end; case A18: x22 in dom g; 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; end; end; hence x11 = x22; end; end; hence x11 = x22; end; hence thesis by FUNCT_1:def 4; end; Lm1: f.:(dom f /\ dom g) c= rng g implies rng f \ rng g c= rng(f+*g) proof assume A1: f.:(dom f /\ dom g) c= rng g; let y1 be object; assume A2: y1 in rng f \ rng g; then consider x1 being object 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 assume x1 in dom g; 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; end; then (f+*g).x1 = f.x1 by A5,FUNCT_4:def 1; hence thesis by A4,A6,FUNCT_1:def 3; end; theorem f.:(dom f /\ dom g) c= rng g implies rng f \/ rng g = rng(f+*g) proof assume f.:(dom f /\ dom g) c= rng 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 thesis by A2,XBOOLE_0:def 10; end; reserve T for T_2 TopSpace; reconsider dwa=2 as Real; theorem for P, Q being Subset of T for p being Point of T, f being Function of I[01], T|P, 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 ex h being Function of I[01], T|(P \/ Q) st h is being_homeomorphism & h.0 = f.0 & h.1 = g .1 proof 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 U(Real) = In(2*$1,REAL); let P, Q be Subset of T; let p be Point of T; let f be Function of I[01], T|P, g be Function of I[01], T|Q; 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; 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 X[object,object] means for a 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 = U(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 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 as Function of R^1,R^1 by TOPMETR:17; A17: dom (f3| [.0,1/2.]) = dom f3 /\ [. 0,1/2 .] by RELAT_1:61 .= REAL /\ [. 0,1/2 .] by FUNCT_2:def 1 .= [. 0,1/2 .] by XBOOLE_1:28 .= the carrier of T1 by TOPMETR:18; rng (f3| [.0,1/2.]) c= the carrier of R^1; then reconsider f39 = f3|PP as Function of T1,R^1 by A17,FUNCT_2:def 1 ,RELSET_1:4; A18: dom f39 = the carrier of T1 by FUNCT_2:def 1; rng f39 c= the carrier of I[01] proof let y be object; assume y in rng f39; 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 as Element of REAL by XREAL_0:def 1; y = f3.x by A19,A20,FUNCT_1:47 .= U(r) by A10,A21; then y in {rr where rr is Real: 0 <= rr & rr <= 1} by A23; hence thesis by BORSUK_1:40,RCOMP_1:def 1; end; then reconsider f4 = f39 as Function of T1,I[01] by A18,RELSET_1:4; A24: R^1|PP = T1 by TOPMETR:19; f3.x = dwa*x + 0 proof reconsider x as Element of REAL by XREAL_0:def 1; f3.x = U(x) + 0 by A10; hence thesis; end; then f39 is continuous by A24,TOPMETR:7,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 as non empty Subset of R^1 by XXREAL_1:1; deffunc U1(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 = U1(x) from FUNCT_2:sch 4; reconsider g3 as Function of R^1,R^1 by TOPMETR:17; A27: dom (g3| [. 1/2,1 .]) = dom g3 /\ [. 1/2,1 .] by RELAT_1:61 .= REAL /\ [. 1/2,1 .] by FUNCT_2:def 1 .= [. 1/2,1 .] by XBOOLE_1:28 .= the carrier of T2 by TOPMETR:18; rng (g3| [. 1/2,1 .]) c= the carrier of R^1; then reconsider g39 = g3|PP as Function of T2,R^1 by A27,FUNCT_2:def 1 ,RELSET_1:4; A28: dom g39 = the carrier of T2 by FUNCT_2:def 1; rng g39 c= the carrier of I[01] proof let y be object; assume y in rng g39; 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 as Element of REAL by XREAL_0:def 1; y = g3.x by A29,A30,FUNCT_1:47 .= U1(r) by A26,A31 .= dwa*r - 1; then y in {rr where rr is Real: 0 <= rr & rr <= 1} by A34,A35; hence thesis by BORSUK_1:40,RCOMP_1:def 1; 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] qua TopSpace) & ([#] T1) /\ ([#] T2) = {pp} by BORSUK_1:40,XXREAL_1:165,418; A37: g3.x = 2*x + (-1) proof reconsider x as Element of REAL by XREAL_0:def 1; g3.x = U1(x) by A26 .= dwa*x -1 .= 2*x + (-1); hence thesis; end; R^1|PP = T2 by TOPMETR:19; then g39 is continuous by A37,TOPMETR:7,21; then A38: g4 is continuous by PRE_TOPC:27; A39: for x being object st x in [. 0,1/2 .] ex u being object st X[x,u] proof let x be object; assume x in [. 0,1/2 .]; then x in { r: 0 <= r & r <= 1/2} by RCOMP_1:def 1; then consider r such that A40: r=x and 0<=r and r<=1/2; take f.(2*r); thus thesis by A40; end; consider f2 being Function such that A41: dom f2 = [. 0,1/2 .] and A42: for x being object st x in [. 0,1/2 .] holds X[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 let y be object; assume y in rng f2; 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: 0 <= a & a <= 1/2 } by A41,A45,RCOMP_1:def 1; then consider a 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,127; then 2*a in { r: 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; end; then A50: rng f2 c= P; P c= P \/ Q by XBOOLE_1:7; then rng f2 c= the carrier of T|(P \/ Q qua Subset of T) by A11,A50; then reconsider f1 = f2 as Function of T1,M|R by A43,FUNCT_2:def 1,RELSET_1:4 ; for x being object st x in the carrier of T1 holds f1.x = (ff*f4).x proof let x be object such that A51: x in the carrier of T1; 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.U(x9) .= f.(f3.x9) by A10 .= f.(f4.x) by A17,A51,FUNCT_1:47 .= (ff*f4).x by A51,FUNCT_2:15; end; then A52: f1 is continuous by A25,A16,FUNCT_2:12; A53: now let x be Real; assume x in dom f2; then x in {a: 0 <= a & a <= 1/2} by A41,RCOMP_1:def 1; then consider a 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,127; then 2*a in { r: 0 <= r & r <= 1 }; hence 2*x in dom f by A44,A54,RCOMP_1:def 1; end; defpred X[object,object] means for a st a=$1 holds $2 = g.(2*a-1); A56: for x being object st x in [. 1/2,1 .] ex u being object st X[x,u] proof let x be object; assume x in [. 1/2,1 .]; then x in { r: 1/2 <= r & r <= 1} by RCOMP_1:def 1; then consider r such that A57: r=x and 1/2<=r and r<=1; take g.(2*r-1); thus thesis by A57; end; consider g2 being Function such that A58: dom g2 = [. 1/2, 1 .] and A59: for x being object st x in [. 1/2,1 .] holds X[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 let y be object; assume y in rng g2; 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: 1/2 <= a & a <= 1 } by A58,A62,RCOMP_1:def 1; then consider a 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: 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; end; then A69: rng g2 c= Q; A70: Q c= rng g2 proof let a be object; assume a in Q; 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 thesis by A77,FUNCT_1:def 3; end; TopSpaceMetr(RealSpace) is T_2 by PCOMPS_1:34; then A78: I[01] is T_2 by TOPMETR:2,def 6; A79: 1/2 in [. 1/2,1 .] by XXREAL_1:1; A80: now let x be Real; assume x in dom g2; then x in {a: 1/2 <= a & a <= 1} by A58,RCOMP_1:def 1; then consider a 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: 0 <= r & r <= 1 } by A84; hence 2*x - 1 in dom g by A61,A81,RCOMP_1:def 1; end; Q c= P \/ Q by XBOOLE_1:7; then rng g2 c= the carrier of M|R by A11,A69; then reconsider g1 = g2 as Function of T2,M|R by A60,FUNCT_2:def 1,RELSET_1:4 ; for x being object st x in the carrier of T2 holds g1.x = (g9*g4).x proof let x be object such that A85: x in the carrier of T2; 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.U1(x9) .= g.(g3.x9) by A26 .= g.(g4.x) by A27,A85,FUNCT_1:47 .= (g9*g4).x by A85,FUNCT_2:15; 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 let x1,x2 be object; assume that A89: x1 in dom h and A90: x2 in dom h and A91: h.x1 = h.x2; now per cases; suppose A92: not x1 in dom g2 & not x2 in dom g2; 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: 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 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: 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 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; end; suppose A100: not x1 in dom g2 & x2 in dom g2; 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: 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 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: 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 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; end; suppose A112: x1 in dom g2 & not x2 in dom g2; 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: 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 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: 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 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; end; suppose A124: x1 in dom g2 & x2 in dom g2; then x2 in { a: 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 as Real; A126: 2*x29-1 in dom g by A80,A124,A125; x1 in { a: 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 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; end; end; hence x1 = x2; 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; A130: 0 in [. 0,1/2 .] by XXREAL_1:1; A131: P c= rng f2 proof let a be object; assume a in P; 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 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 thesis by A136,FUNCT_1:def 3; end; A137: P c= rng h proof let a be object; assume a in P; then consider x being object such that A138: x in dom f2 and A139: a = f2.x by A131,FUNCT_1:def 3; now per cases; suppose A140: x in [. 1/2,1 .]; 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 thesis by A139,A141,A142,FUNCT_1:def 3; end; suppose A144: not x in [. 1/2,1 .]; 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 thesis by A139,A146,FUNCT_1:def 3; end; end; hence thesis; end; rng h c= rng f2 \/ rng g2 & rng f2 \/ rng g2 c= P \/ Q by A50,A69,FUNCT_4:17 ,XBOOLE_1:13; then A147: rng h c= P \/ Q; rng g2 c= rng h by FUNCT_4:18; then Q c= rng h by A70; then P \/ Q c= rng h by A137,XBOOLE_1:8; then rng h = P \/ Q by A147,XBOOLE_0:def 10; then A148: rng h = [#] (M|R) by PRE_TOPC:def 5; I[01] is compact & M|R is T_2 by HEINE:4,TOPMETR:2,20; hence h9 is being_homeomorphism by A148,A129,COMPTS_1:17; 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; 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; end;