topmetr2.miz



    begin

    reserve x,r,a for Real;

    reserve f,g for Function,

x1,x2 for set;

    theorem :: TOPMETR2:1

    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 be 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 :: TOPMETR2:2

    (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 :: TOPMETR2:3

    for P,Q be Subset of T holds for p be Point of T, f be Function of I[01] , (T | P), g be 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 be 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 be 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 be Function of REAL , REAL such that

       A10: for x be 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 be 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 be Real : 0 <= r & r <= (1 / 2) } by RCOMP_1:def 1;

        then

        consider r be 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 be 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, 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 as non empty Subset of R^1 by XXREAL_1: 1;

      deffunc U1( Real) = ( In (((2 * $1) - 1), REAL ));

      consider g3 be Function of REAL , REAL such that

       A26: for x be 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 be 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 be Real : (1 / 2) <= r & r <= 1 } by RCOMP_1:def 1;

        then

        consider r be 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 be 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, XXREAL_1: 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, TOPMETR: 21;

      then

       A38: g4 is continuous by PRE_TOPC: 27;

      

       A39: for x be object st x in [. 0 , (1 / 2).] holds ex u be 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 be Function such that

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

       A42: for x be 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 be 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, XREAL_1: 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 be 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, XREAL_1: 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 be object st x in [.(1 / 2), 1.] holds ex u be 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 be Function such that

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

       A59: for x be 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 be 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 be object such that

         A71: x in ( dom g) and

         A72: a = (g . x) by A8, FUNCT_1:def 3;

        x in { r where r be Real : 0 <= r & r <= 1 } by A61, A71, RCOMP_1:def 1;

        then

        consider x9 be 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 be 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, TOPMETR: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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be object such that

         A132: x in ( dom f) and

         A133: a = (f . x) by A15, FUNCT_1:def 3;

        x in { r where r be Real : 0 <= r & r <= 1 } by A44, A132, RCOMP_1:def 1;

        then

        consider x9 be 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 be 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 be 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, TOPMETR: 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;