partfun4.miz

    begin

    reserve T for non empty TopSpace,

f,g for continuous RealMap of T,

r for Real;

    registration

      let T, f, g;

      set c = the carrier of T;

      reconsider F = f, G = g as continuous Function of T, R^1 by JORDAN5A: 27, TOPMETR: 17;

      cluster (f + g) -> continuous;

      coherence

      proof

        consider H be Function of T, R^1 such that

         A1: for p be Point of T, r1,r2 be Real st (F . p) = r1 & (G . p) = r2 holds (H . p) = (r1 + r2) and

         A2: H is continuous by JGRAPH_2: 19;

        reconsider h = H as RealMap of T by TOPMETR: 17;



         A3: ( dom h) = (c /\ c) by FUNCT_2:def 1

        .= (c /\ ( dom g)) by FUNCT_2:def 1

        .= (( dom f) /\ ( dom g)) by FUNCT_2:def 1;

        for c be object st c in ( dom h) holds (h . c) = ((f . c) + (g . c)) by A1;

        then h = (f + g) by A3, VALUED_1:def 1;

        hence thesis by A2, JORDAN5A: 27;

      end;

      cluster (f - g) -> continuous;

      coherence

      proof

        consider H be Function of T, R^1 such that

         A4: for p be Point of T, r1,r2 be Real st (F . p) = r1 & (G . p) = r2 holds (H . p) = (r1 - r2) and

         A5: H is continuous by JGRAPH_2: 21;

        reconsider h = H as RealMap of T by TOPMETR: 17;



         A6: ( dom h) = (c /\ c) by FUNCT_2:def 1

        .= (c /\ ( dom g)) by FUNCT_2:def 1

        .= (( dom f) /\ ( dom g)) by FUNCT_2:def 1;

        ( dom (f - g)) = (( dom f) /\ ( dom g)) & for c be object st c in ( dom h) holds (h . c) = ((f . c) - (g . c)) by A4, VALUED_1: 12;

        then h = (f - g) by A6, VALUED_1: 14;

        hence thesis by A5, JORDAN5A: 27;

      end;

      cluster (f (#) g) -> continuous;

      coherence

      proof

        consider H be Function of T, R^1 such that

         A7: for p be Point of T, r1,r2 be Real st (F . p) = r1 & (G . p) = r2 holds (H . p) = (r1 * r2) and

         A8: H is continuous by JGRAPH_2: 25;

        reconsider h = H as RealMap of T by TOPMETR: 17;



         A9: ( dom h) = (c /\ c) by FUNCT_2:def 1

        .= (c /\ ( dom g)) by FUNCT_2:def 1

        .= (( dom f) /\ ( dom g)) by FUNCT_2:def 1;

        for c be object st c in ( dom h) holds (h . c) = ((f . c) * (g . c)) by A7;

        then h = (f (#) g) by A9, VALUED_1:def 4;

        hence thesis by A8, JORDAN5A: 27;

      end;

    end

    registration

      let T, f;

      cluster ( - f) -> continuous;

      coherence

      proof

        reconsider F = f as continuous Function of T, R^1 by JORDAN5A: 27, TOPMETR: 17;

        set c = the carrier of T;

        consider H be Function of T, R^1 such that

         A1: for p be Point of T, r1 be Real st (F . p) = r1 holds (H . p) = ( - r1) and

         A2: H is continuous by JGRAPH_4: 8;

        reconsider h = H as RealMap of T by TOPMETR: 17;



         A3: ( dom h) = c by FUNCT_2:def 1

        .= ( dom f) by FUNCT_2:def 1;

        for c be object st c in ( dom h) holds (h . c) = ( - (f . c)) by A1;

        then h = ( - f) by A3, VALUED_1: 9;

        hence thesis by A2, JORDAN5A: 27;

      end;

    end

    registration

      let T, f;

      cluster ( abs f) -> continuous;

      coherence

      proof

        reconsider F = f as continuous Function of T, R^1 by JORDAN5A: 27, TOPMETR: 17;

        set c = the carrier of T;

        consider H be Function of T, R^1 such that

         A1: for p be Point of T, r1 be Real st (F . p) = r1 holds (H . p) = |.r1.| and

         A2: H is continuous by JGRAPH_4: 7;

        reconsider h = H as RealMap of T by TOPMETR: 17;



         A3: ( dom h) = c by FUNCT_2:def 1

        .= ( dom f) by FUNCT_2:def 1;

        for c be object st c in ( dom h) holds (h . c) = |.(f . c).| by A1;

        then h = ( abs f) by A3, VALUED_1:def 11;

        hence thesis by A2, JORDAN5A: 27;

      end;

    end

     Lm1:

    now

      let T;

      let a be Element of REAL ;

      set c = the carrier of T;

      set f = (c --> a);

      thus f is continuous

      proof

        let Y be Subset of REAL ;



         A1: ( dom f) = c by FUNCT_2:def 1;

        assume Y is closed;



         A2: ( rng f) = {a} by FUNCOP_1: 8;

        per cases ;

          suppose a in Y;

          then

           A3: ( rng f) c= Y by A2, ZFMISC_1: 31;

          (f " Y) = (f " (( rng f) /\ Y)) by RELAT_1: 133

          .= (f " ( rng f)) by A3, XBOOLE_1: 28

          .= c by A1, RELAT_1: 134

          .= ( [#] T);

          hence thesis;

        end;

          suppose not a in Y;

          then

           A4: ( rng f) misses Y by A2, ZFMISC_1: 50;

          (f " Y) = (f " (( rng f) /\ Y)) by RELAT_1: 133

          .= (f " {} ) by A4, XBOOLE_0:def 7

          .= ( {} T);

          hence thesis;

        end;

      end;

    end;

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

    registration

      let T;

      cluster positive-yielding continuous for RealMap of T;

      existence

      proof

        take f = (the carrier of T --> jj);

        thus f is positive-yielding;

        thus thesis by Lm1;

      end;

      cluster negative-yielding continuous for RealMap of T;

      existence

      proof

        take f = (the carrier of T --> ( - jj));

        thus f is negative-yielding;

        thus thesis by Lm1;

      end;

    end

    registration

      let T;

      let f be nonnegative-yielding continuous RealMap of T;

      cluster ( sqrt f) -> continuous;

      coherence

      proof

        reconsider F = f as continuous Function of T, R^1 by JORDAN5A: 27, TOPMETR: 17;

        set c = the carrier of T;

        for q be Point of T holds ex r be Real st (f . q) = r & r >= 0

        proof

          let q be Point of T;

          take (f . q);

          thus (f . q) = (f . q);

          ( dom f) = c by FUNCT_2:def 1;

          then (f . q) in ( rng f) by FUNCT_1:def 3;

          hence thesis by PARTFUN3:def 4;

        end;

        then

        consider H be Function of T, R^1 such that

         A1: for p be Point of T, r1 be Real st (F . p) = r1 holds (H . p) = ( sqrt r1) and

         A2: H is continuous by JGRAPH_3: 5;

        reconsider h = H as RealMap of T by TOPMETR: 17;



         A3: ( dom h) = c by FUNCT_2:def 1

        .= ( dom f) by FUNCT_2:def 1;

        for c be object st c in ( dom h) holds (h . c) = ( sqrt (f . c)) by A1;

        then h = ( sqrt f) by A3, PARTFUN3:def 5;

        hence thesis by A2, JORDAN5A: 27;

      end;

    end

    registration

      let T, f, r;

      cluster (r (#) f) -> continuous;

      coherence

      proof

        reconsider F = f as continuous Function of T, R^1 by JORDAN5A: 27, TOPMETR: 17;

        set c = the carrier of T;

        consider H be Function of T, R^1 such that

         A1: for p be Point of T, r1 be Real st (F . p) = r1 holds (H . p) = (r * r1) and

         A2: H is continuous by JGRAPH_2: 23;

        reconsider h = H as RealMap of T by TOPMETR: 17;



         A3: ( dom h) = c by FUNCT_2:def 1

        .= ( dom f) by FUNCT_2:def 1;

        for c be object st c in ( dom h) holds (h . c) = (r * (f . c)) by A1;

        then h = (r (#) f) by A3, VALUED_1:def 5;

        hence thesis by A2, JORDAN5A: 27;

      end;

    end

    registration

      let T;

      let f be non-empty continuous RealMap of T;

      cluster (f ^ ) -> continuous;

      coherence

      proof

        reconsider F = f as continuous Function of T, R^1 by JORDAN5A: 27, TOPMETR: 17;

        set c = the carrier of T;

        for q be Point of T holds (f . q) <> 0

        proof

          let q be Point of T;

          ( dom f) = c by FUNCT_2:def 1;

          hence thesis;

        end;

        then

        consider H be Function of T, R^1 such that

         A1: for p be Point of T, r1 be Real st (F . p) = r1 holds (H . p) = (1 / r1) and

         A2: H is continuous by JGRAPH_2: 26;

        reconsider h = H as RealMap of T by TOPMETR: 17;

         A3:

        now

          let a be object;

          assume a in ( dom h);



          hence (h . a) = (1 / (f . a)) by A1

          .= (1 * ((f . a) " )) by XCMPLX_0:def 9

          .= ((f . a) " );

        end;

        ( dom h) = c by FUNCT_2:def 1

        .= (( dom f) \ (f " { 0 })) by FUNCT_2:def 1;

        then h = (f ^ ) by A3, RFUNCT_1:def 2;

        hence thesis by A2, JORDAN5A: 27;

      end;

    end

    registration

      let T, f;

      let g be non-empty continuous RealMap of T;

      cluster (f / g) -> continuous;

      coherence

      proof

        reconsider F = f, G = g as continuous Function of T, R^1 by JORDAN5A: 27, TOPMETR: 17;

        set c = the carrier of T;

        for q be Point of T holds (g . q) <> 0

        proof

          let q be Point of T;

          ( dom g) = c by FUNCT_2:def 1;

          hence thesis;

        end;

        then

        consider H be Function of T, R^1 such that

         A1: for p be Point of T, r1,r2 be Real st (F . p) = r1 & (G . p) = r2 holds (H . p) = (r1 / r2) and

         A2: H is continuous by JGRAPH_2: 27;

        reconsider h = H as RealMap of T by TOPMETR: 17;

         A3:

        now

          let c be object;

          assume c in ( dom h);



          hence (h . c) = ((f . c) / (g . c)) by A1

          .= ((f . c) * ((g . c) " )) by XCMPLX_0:def 9;

        end;

        ( dom h) = (c /\ c) by FUNCT_2:def 1

        .= (c /\ ( dom g)) by FUNCT_2:def 1

        .= (( dom f) /\ (( dom g) \ (g " { 0 }))) by FUNCT_2:def 1;

        then h = (f / g) by A3, RFUNCT_1:def 1;

        hence thesis by A2, JORDAN5A: 27;

      end;

    end