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