partfun3.miz



    begin

    registration

      let r be Real;

      cluster (r / r) -> non negative;

      coherence

      proof

        r <= 0 or 0 <= r;

        hence thesis;

      end;

    end

    registration

      let r be Real;

      cluster (r * r) -> non negative;

      coherence by XREAL_1: 63;

      cluster (r * (r " )) -> non negative;

      coherence

      proof

        (r * (r " )) = (r / r) by XCMPLX_0:def 9;

        hence thesis;

      end;

    end

    registration

      let r be non negative Real;

      cluster ( sqrt r) -> non negative;

      coherence by SQUARE_1:def 2;

    end

    registration

      let r be positive Real;

      cluster ( sqrt r) -> positive;

      coherence by SQUARE_1: 25;

    end

    theorem :: PARTFUN3:1

    for f be Function, A be set st f is one-to-one & A c= ( dom (f " )) holds (f .: ((f " ) .: A)) = A

    proof

      let f be Function, A be set;

      assume that

       A1: f is one-to-one and

       A2: A c= ( dom (f " ));

      (((f " ) " ) .: ((f " ) .: A)) = A by A1, A2, FUNCT_1: 107;

      hence thesis by A1, FUNCT_1: 43;

    end;

    registration

      let f be non-empty Function;

      cluster (f " { 0 }) -> empty;

      coherence

      proof

        assume not thesis;

        then

        consider x be object such that

         A1: x in (f " { 0 }) by XBOOLE_0:def 1;

        x in ( dom f) by A1, FUNCT_1:def 7;

        then

         A2: (f . x) in ( rng f) by FUNCT_1:def 3;

        (f . x) in { 0 } by A1, FUNCT_1:def 7;

        then (f . x) = 0 by TARSKI:def 1;

        hence thesis by A2;

      end;

    end

    definition

      let R be Relation;

      :: PARTFUN3:def1

      attr R is positive-yielding means

      : Def1: for r be Real st r in ( rng R) holds 0 < r;

      :: PARTFUN3:def2

      attr R is negative-yielding means

      : Def2: for r be Real st r in ( rng R) holds 0 > r;

      :: PARTFUN3:def3

      attr R is nonpositive-yielding means

      : Def3: for r be Real st r in ( rng R) holds 0 >= r;

      :: PARTFUN3:def4

      attr R is nonnegative-yielding means

      : Def4: for r be Real st r in ( rng R) holds 0 <= r;

    end

    registration

      let X be set, r be positive Real;

      cluster (X --> r) -> positive-yielding;

      coherence

      proof

        let x be Real;

        assume x in ( rng (X --> r));

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let X be set, r be negative Real;

      cluster (X --> r) -> negative-yielding;

      coherence

      proof

        let x be Real;

        assume x in ( rng (X --> r));

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let X be set, r be non positive Real;

      cluster (X --> r) -> nonpositive-yielding;

      coherence

      proof

        let x be Real;

        assume x in ( rng (X --> r));

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let X be set, r be non negative Real;

      cluster (X --> r) -> nonnegative-yielding;

      coherence

      proof

        let x be Real;

        assume x in ( rng (X --> r));

        hence thesis by TARSKI:def 1;

      end;

    end

    registration

      let X be non empty set;

      cluster (X --> 0 ) -> non non-empty;

      coherence

      proof

        ( rng (X --> 0 )) = { 0 } by FUNCOP_1: 8;

        hence {} in ( rng (X --> 0 )) by TARSKI:def 1;

      end;

    end

    registration

      cluster positive-yielding -> nonnegative-yielding non-empty for Relation;

      coherence ;

      cluster negative-yielding -> nonpositive-yielding non-empty for Relation;

      coherence ;

    end

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

    registration

      let X be set;

      cluster negative-yielding for Function of X, REAL ;

      existence

      proof

        take (X --> ( - jj));

        thus thesis;

      end;

      cluster positive-yielding for Function of X, REAL ;

      existence

      proof

        take (X --> jj);

        thus thesis;

      end;

    end

    registration

      cluster non-empty real-valued for Function;

      existence

      proof

        set f = the non-empty Function of 0 , REAL ;

        take f;

        thus thesis;

      end;

    end

    theorem :: PARTFUN3:2

    

     Th2: for f be non-empty real-valued Function holds ( dom (f ^ )) = ( dom f)

    proof

      let f be non-empty real-valued Function;

      

      thus ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2

      .= ( dom f);

    end;

    theorem :: PARTFUN3:3

    

     Th3: for X be non empty set, f be PartFunc of X, REAL , g be non-empty PartFunc of X, REAL holds ( dom (f / g)) = (( dom f) /\ ( dom g))

    proof

      let X be non empty set, f be PartFunc of X, REAL , g be non-empty PartFunc of X, REAL ;

      

      thus ( dom (f / g)) = (( dom f) /\ (( dom g) \ (g " { 0 }))) by RFUNCT_1:def 1

      .= (( dom f) /\ ( dom g));

    end;

    registration

      let X be set;

      let f,g be nonpositive-yielding PartFunc of X, REAL ;

      cluster (f + g) -> nonpositive-yielding;

      coherence

      proof

        let r be Real;

        set R = (f + g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1:def 1;

        then x in ( dom g) by A1, XBOOLE_0:def 4;

        then

         A4: (g . x) in ( rng g) by FUNCT_1:def 3;

        x in ( dom f) by A1, A3, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x), b = (g . x) as non positive Real by A4, Def3;

        (a + b) is non positive;

        hence thesis by A1, A2, VALUED_1:def 1;

      end;

    end

    registration

      let X be set;

      let f,g be nonnegative-yielding PartFunc of X, REAL ;

      cluster (f + g) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f + g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1:def 1;

        then x in ( dom g) by A1, XBOOLE_0:def 4;

        then

         A4: (g . x) in ( rng g) by FUNCT_1:def 3;

        x in ( dom f) by A1, A3, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x), b = (g . x) as non negative Real by A4, Def4;

        (a + b) is non negative;

        hence thesis by A1, A2, VALUED_1:def 1;

      end;

    end

    registration

      let X be set;

      let f be positive-yielding PartFunc of X, REAL ;

      let g be nonnegative-yielding PartFunc of X, REAL ;

      cluster (f + g) -> positive-yielding;

      coherence

      proof

        let r be Real;

        set R = (f + g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1:def 1;

        then x in ( dom f) by A1, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x) as positive Real by Def1;

        x in ( dom g) by A1, A3, XBOOLE_0:def 4;

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider b = (g . x) as non negative Real by Def4;

        (a + b) is positive;

        hence thesis by A1, A2, VALUED_1:def 1;

      end;

    end

    registration

      let X be set;

      let f be nonnegative-yielding PartFunc of X, REAL ;

      let g be positive-yielding PartFunc of X, REAL ;

      cluster (f + g) -> positive-yielding;

      coherence ;

    end

    registration

      let X be set;

      let f be nonpositive-yielding PartFunc of X, REAL ;

      let g be negative-yielding PartFunc of X, REAL ;

      cluster (f + g) -> negative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f + g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1:def 1;

        then x in ( dom f) by A1, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x) as non positive Real by Def3;

        x in ( dom g) by A1, A3, XBOOLE_0:def 4;

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider b = (g . x) as negative Real by Def2;

        (a + b) is negative;

        hence thesis by A1, A2, VALUED_1:def 1;

      end;

    end

    registration

      let X be set;

      let f be negative-yielding PartFunc of X, REAL ;

      let g be nonpositive-yielding PartFunc of X, REAL ;

      cluster (f + g) -> negative-yielding;

      coherence ;

    end

    registration

      let X be set;

      let f be nonnegative-yielding PartFunc of X, REAL ;

      let g be nonpositive-yielding PartFunc of X, REAL ;

      cluster (f - g) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f - g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

        then x in ( dom f) by A1, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x) as non negative Real by Def4;

        x in ( dom g) by A1, A3, XBOOLE_0:def 4;

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider b = (g . x) as non positive Real by Def3;

        (a - b) is non negative;

        hence thesis by A1, A2, VALUED_1: 13;

      end;

    end

    registration

      let X be set;

      let f be nonpositive-yielding PartFunc of X, REAL ;

      let g be nonnegative-yielding PartFunc of X, REAL ;

      cluster (f - g) -> nonpositive-yielding;

      coherence

      proof

        let r be Real;

        set R = (f - g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

        then x in ( dom f) by A1, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x) as non positive Real by Def3;

        x in ( dom g) by A1, A3, XBOOLE_0:def 4;

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider b = (g . x) as non negative Real by Def4;

        (a - b) is non positive;

        hence thesis by A1, A2, VALUED_1: 13;

      end;

    end

    registration

      let X be set;

      let f be positive-yielding PartFunc of X, REAL ;

      let g be nonpositive-yielding PartFunc of X, REAL ;

      cluster (f - g) -> positive-yielding;

      coherence

      proof

        let r be Real;

        set R = (f - g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

        then x in ( dom f) by A1, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x) as positive Real by Def1;

        x in ( dom g) by A1, A3, XBOOLE_0:def 4;

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider b = (g . x) as non positive Real by Def3;

        (a - b) is positive;

        hence thesis by A1, A2, VALUED_1: 13;

      end;

    end

    registration

      let X be set;

      let f be nonpositive-yielding PartFunc of X, REAL ;

      let g be positive-yielding PartFunc of X, REAL ;

      cluster (f - g) -> negative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f - g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

        then x in ( dom f) by A1, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x) as non positive Real by Def3;

        x in ( dom g) by A1, A3, XBOOLE_0:def 4;

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider b = (g . x) as positive Real by Def1;

        (a - b) is negative;

        hence thesis by A1, A2, VALUED_1: 13;

      end;

    end

    registration

      let X be set;

      let f be negative-yielding PartFunc of X, REAL ;

      let g be nonnegative-yielding PartFunc of X, REAL ;

      cluster (f - g) -> negative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f - g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

        then x in ( dom f) by A1, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x) as negative Real by Def2;

        x in ( dom g) by A1, A3, XBOOLE_0:def 4;

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider b = (g . x) as non negative Real by Def4;

        (a - b) is negative;

        hence thesis by A1, A2, VALUED_1: 13;

      end;

    end

    registration

      let X be set;

      let f be nonnegative-yielding PartFunc of X, REAL ;

      let g be negative-yielding PartFunc of X, REAL ;

      cluster (f - g) -> positive-yielding;

      coherence

      proof

        let r be Real;

        set R = (f - g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1: 12;

        then x in ( dom f) by A1, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x) as non negative Real by Def4;

        x in ( dom g) by A1, A3, XBOOLE_0:def 4;

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider b = (g . x) as negative Real by Def2;

        (a - b) is positive;

        hence thesis by A1, A2, VALUED_1: 13;

      end;

    end

    registration

      let X be set;

      let f,g be nonpositive-yielding PartFunc of X, REAL ;

      cluster (f (#) g) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f (#) g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1:def 4;

        then x in ( dom g) by A1, XBOOLE_0:def 4;

        then

         A4: (g . x) in ( rng g) by FUNCT_1:def 3;

        x in ( dom f) by A1, A3, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x), b = (g . x) as non positive Real by A4, Def3;

        (a * b) is non negative;

        hence thesis by A2, VALUED_1: 5;

      end;

    end

    registration

      let X be set;

      let f,g be nonnegative-yielding PartFunc of X, REAL ;

      cluster (f (#) g) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f (#) g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1:def 4;

        then x in ( dom g) by A1, XBOOLE_0:def 4;

        then

         A4: (g . x) in ( rng g) by FUNCT_1:def 3;

        x in ( dom f) by A1, A3, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x), b = (g . x) as non negative Real by A4, Def4;

        (a * b) is non negative;

        hence thesis by A2, VALUED_1: 5;

      end;

    end

    registration

      let X be set;

      let f be nonpositive-yielding PartFunc of X, REAL ;

      let g be nonnegative-yielding PartFunc of X, REAL ;

      cluster (f (#) g) -> nonpositive-yielding;

      coherence

      proof

        let r be Real;

        set R = (f (#) g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1:def 4;

        then x in ( dom f) by A1, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x) as non positive Real by Def3;

        x in ( dom g) by A1, A3, XBOOLE_0:def 4;

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider b = (g . x) as non negative Real by Def4;

        (a * b) is non positive;

        hence thesis by A2, VALUED_1: 5;

      end;

    end

    registration

      let X be set;

      let f be nonnegative-yielding PartFunc of X, REAL ;

      let g be nonpositive-yielding PartFunc of X, REAL ;

      cluster (f (#) g) -> nonpositive-yielding;

      coherence ;

    end

    registration

      let X be set;

      let f be positive-yielding PartFunc of X, REAL ;

      let g be negative-yielding PartFunc of X, REAL ;

      cluster (f (#) g) -> negative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f (#) g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1:def 4;

        then x in ( dom f) by A1, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x) as positive Real by Def1;

        x in ( dom g) by A1, A3, XBOOLE_0:def 4;

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider b = (g . x) as negative Real by Def2;

        (a * b) is negative;

        hence thesis by A2, VALUED_1: 5;

      end;

    end

    registration

      let X be set;

      let f be negative-yielding PartFunc of X, REAL ;

      let g be positive-yielding PartFunc of X, REAL ;

      cluster (f (#) g) -> negative-yielding;

      coherence ;

    end

    registration

      let X be set;

      let f,g be positive-yielding PartFunc of X, REAL ;

      cluster (f (#) g) -> positive-yielding;

      coherence

      proof

        let r be Real;

        set R = (f (#) g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1:def 4;

        then x in ( dom g) by A1, XBOOLE_0:def 4;

        then

         A4: (g . x) in ( rng g) by FUNCT_1:def 3;

        x in ( dom f) by A1, A3, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x), b = (g . x) as positive Real by A4, Def1;

        (a * b) is positive;

        hence thesis by A2, VALUED_1: 5;

      end;

    end

    registration

      let X be set;

      let f,g be negative-yielding PartFunc of X, REAL ;

      cluster (f (#) g) -> positive-yielding;

      coherence

      proof

        let r be Real;

        set R = (f (#) g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1:def 4;

        then x in ( dom g) by A1, XBOOLE_0:def 4;

        then

         A4: (g . x) in ( rng g) by FUNCT_1:def 3;

        x in ( dom f) by A1, A3, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x), b = (g . x) as negative Real by A4, Def2;

        (a * b) is positive;

        hence thesis by A2, VALUED_1: 5;

      end;

    end

    registration

      let X be set;

      let f,g be non-empty PartFunc of X, REAL ;

      cluster (f (#) g) -> non-empty;

      coherence

      proof

        set R = (f (#) g);

        assume not thesis;

        then 0 in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = 0 by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ ( dom g)) by VALUED_1:def 4;

        then x in ( dom g) by A1, XBOOLE_0:def 4;

        then

         A4: (g . x) in ( rng g) by FUNCT_1:def 3;

        x in ( dom f) by A1, A3, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x), b = (g . x) as non zero Real by A4;

        (a * b) is non zero;

        hence thesis by A2, VALUED_1: 5;

      end;

    end

    registration

      let X be set;

      let f be PartFunc of X, REAL ;

      cluster (f (#) f) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f (#) f);

        assume r in ( rng R);

        then

        consider x be object such that x in ( dom R) and

         A1: (R . x) = r by FUNCT_1:def 3;

        ((f . x) * (f . x)) is non negative;

        hence thesis by A1, VALUED_1: 5;

      end;

    end

    registration

      let X be set;

      let r be non positive Real;

      let f be nonpositive-yielding PartFunc of X, REAL ;

      cluster (r (#) f) -> nonnegative-yielding;

      coherence

      proof

        let z be Real;

        set R = (r (#) f);

        assume z in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = z by FUNCT_1:def 3;

        ( dom R) = ( dom f) by VALUED_1:def 5;

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as non positive Real by Def3;

        (r * a) is non negative;

        hence thesis by A1, A2, VALUED_1:def 5;

      end;

    end

    registration

      let X be set;

      let r be non negative Real;

      let f be nonnegative-yielding PartFunc of X, REAL ;

      cluster (r (#) f) -> nonnegative-yielding;

      coherence

      proof

        let z be Real;

        set R = (r (#) f);

        assume z in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = z by FUNCT_1:def 3;

        ( dom R) = ( dom f) by VALUED_1:def 5;

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as non negative Real by Def4;

        (r * a) is non negative;

        hence thesis by A1, A2, VALUED_1:def 5;

      end;

    end

    registration

      let X be set;

      let r be non positive Real;

      let f be nonnegative-yielding PartFunc of X, REAL ;

      cluster (r (#) f) -> nonpositive-yielding;

      coherence

      proof

        let z be Real;

        set R = (r (#) f);

        assume z in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = z by FUNCT_1:def 3;

        ( dom R) = ( dom f) by VALUED_1:def 5;

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as non negative Real by Def4;

        (r * a) is non positive;

        hence thesis by A1, A2, VALUED_1:def 5;

      end;

    end

    registration

      let X be set;

      let r be non negative Real;

      let f be nonpositive-yielding PartFunc of X, REAL ;

      cluster (r (#) f) -> nonpositive-yielding;

      coherence

      proof

        let z be Real;

        set R = (r (#) f);

        assume z in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = z by FUNCT_1:def 3;

        ( dom R) = ( dom f) by VALUED_1:def 5;

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as non positive Real by Def3;

        (r * a) is non positive;

        hence thesis by A1, A2, VALUED_1:def 5;

      end;

    end

    registration

      let X be set;

      let r be positive Real;

      let f be negative-yielding PartFunc of X, REAL ;

      cluster (r (#) f) -> negative-yielding;

      coherence

      proof

        let z be Real;

        set R = (r (#) f);

        assume z in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = z by FUNCT_1:def 3;

        ( dom R) = ( dom f) by VALUED_1:def 5;

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as negative Real by Def2;

        (r * a) is negative;

        hence thesis by A1, A2, VALUED_1:def 5;

      end;

    end

    registration

      let X be set;

      let r be negative Real;

      let f be positive-yielding PartFunc of X, REAL ;

      cluster (r (#) f) -> negative-yielding;

      coherence

      proof

        let z be Real;

        set R = (r (#) f);

        assume z in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = z by FUNCT_1:def 3;

        ( dom R) = ( dom f) by VALUED_1:def 5;

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as positive Real by Def1;

        (r * a) is negative;

        hence thesis by A1, A2, VALUED_1:def 5;

      end;

    end

    registration

      let X be set;

      let r be positive Real;

      let f be positive-yielding PartFunc of X, REAL ;

      cluster (r (#) f) -> positive-yielding;

      coherence

      proof

        let z be Real;

        set R = (r (#) f);

        assume z in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = z by FUNCT_1:def 3;

        ( dom R) = ( dom f) by VALUED_1:def 5;

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as positive Real by Def1;

        (r * a) is positive;

        hence thesis by A1, A2, VALUED_1:def 5;

      end;

    end

    registration

      let X be set;

      let r be negative Real;

      let f be negative-yielding PartFunc of X, REAL ;

      cluster (r (#) f) -> positive-yielding;

      coherence

      proof

        let z be Real;

        set R = (r (#) f);

        assume z in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = z by FUNCT_1:def 3;

        ( dom R) = ( dom f) by VALUED_1:def 5;

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as negative Real by Def2;

        (r * a) is positive;

        hence thesis by A1, A2, VALUED_1:def 5;

      end;

    end

    registration

      let X be set;

      let r be non zero Real;

      let f be non-empty PartFunc of X, REAL ;

      cluster (r (#) f) -> non-empty;

      coherence

      proof

        set R = (r (#) f);

        assume not thesis;

        then 0 in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = 0 by FUNCT_1:def 3;

        ( dom R) = ( dom f) by VALUED_1:def 5;

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as non zero Real;

        (r * a) is non zero;

        hence thesis by A1, A2, VALUED_1:def 5;

      end;

    end

    registration

      let X be non empty set;

      let f,g be nonpositive-yielding PartFunc of X, REAL ;

      cluster (f / g) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f / g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ (( dom g) \ (g " { 0 }))) by RFUNCT_1:def 1;

        then x in (( dom g) \ (g " { 0 })) by A1, XBOOLE_0:def 4;

        then x in ( dom g) by XBOOLE_0:def 5;

        then

         A4: (g . x) in ( rng g) by FUNCT_1:def 3;

        x in ( dom f) by A1, A3, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x), b = (g . x) as non positive Real by A4, Def3;

        (a * (b " )) is non negative;

        hence thesis by A1, A2, RFUNCT_1:def 1;

      end;

    end

    registration

      let X be non empty set;

      let f,g be nonnegative-yielding PartFunc of X, REAL ;

      cluster (f / g) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f / g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ (( dom g) \ (g " { 0 }))) by RFUNCT_1:def 1;

        then x in (( dom g) \ (g " { 0 })) by A1, XBOOLE_0:def 4;

        then x in ( dom g) by XBOOLE_0:def 5;

        then

         A4: (g . x) in ( rng g) by FUNCT_1:def 3;

        x in ( dom f) by A1, A3, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x), b = (g . x) as non negative Real by A4, Def4;

        (a * (b " )) is non negative;

        hence thesis by A1, A2, RFUNCT_1:def 1;

      end;

    end

    registration

      let X be non empty set;

      let f be nonpositive-yielding PartFunc of X, REAL ;

      let g be nonnegative-yielding PartFunc of X, REAL ;

      cluster (f / g) -> nonpositive-yielding;

      coherence

      proof

        let r be Real;

        set R = (f / g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ (( dom g) \ (g " { 0 }))) by RFUNCT_1:def 1;

        then x in ( dom f) by A1, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x) as non positive Real by Def3;

        x in (( dom g) \ (g " { 0 })) by A1, A3, XBOOLE_0:def 4;

        then x in ( dom g) by XBOOLE_0:def 5;

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider b = (g . x) as non negative Real by Def4;

        (a * (b " )) is non positive;

        hence thesis by A1, A2, RFUNCT_1:def 1;

      end;

    end

    registration

      let X be non empty set;

      let f be nonnegative-yielding PartFunc of X, REAL ;

      let g be nonpositive-yielding PartFunc of X, REAL ;

      cluster (f / g) -> nonpositive-yielding;

      coherence

      proof

        let r be Real;

        set R = (f / g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ (( dom g) \ (g " { 0 }))) by RFUNCT_1:def 1;

        then x in ( dom f) by A1, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x) as non negative Real by Def4;

        x in (( dom g) \ (g " { 0 })) by A1, A3, XBOOLE_0:def 4;

        then x in ( dom g) by XBOOLE_0:def 5;

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider b = (g . x) as non positive Real by Def3;

        (a * (b " )) is non positive;

        hence thesis by A1, A2, RFUNCT_1:def 1;

      end;

    end

    registration

      let X be non empty set;

      let f be positive-yielding PartFunc of X, REAL ;

      let g be negative-yielding PartFunc of X, REAL ;

      cluster (f / g) -> negative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f / g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ (( dom g) \ (g " { 0 }))) by RFUNCT_1:def 1;

        then x in ( dom f) by A1, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x) as positive Real by Def1;

        x in (( dom g) \ (g " { 0 })) by A1, A3, XBOOLE_0:def 4;

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider b = (g . x) as negative Real by Def2;

        (a * (b " )) is negative;

        hence thesis by A1, A2, RFUNCT_1:def 1;

      end;

    end

    registration

      let X be non empty set;

      let f be negative-yielding PartFunc of X, REAL ;

      let g be positive-yielding PartFunc of X, REAL ;

      cluster (f / g) -> negative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f / g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ (( dom g) \ (g " { 0 }))) by RFUNCT_1:def 1;

        then x in ( dom f) by A1, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x) as negative Real by Def2;

        x in (( dom g) \ (g " { 0 })) by A1, A3, XBOOLE_0:def 4;

        then (g . x) in ( rng g) by FUNCT_1:def 3;

        then

        reconsider b = (g . x) as positive Real by Def1;

        (a * (b " )) is negative;

        hence thesis by A1, A2, RFUNCT_1:def 1;

      end;

    end

    registration

      let X be non empty set;

      let f,g be positive-yielding PartFunc of X, REAL ;

      cluster (f / g) -> positive-yielding;

      coherence

      proof

        let r be Real;

        set R = (f / g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ (( dom g) \ (g " { 0 }))) by RFUNCT_1:def 1;

        then x in (( dom g) \ (g " { 0 })) by A1, XBOOLE_0:def 4;

        then

         A4: (g . x) in ( rng g) by FUNCT_1:def 3;

        x in ( dom f) by A1, A3, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x), b = (g . x) as positive Real by A4, Def1;

        (a * (b " )) is positive;

        hence thesis by A1, A2, RFUNCT_1:def 1;

      end;

    end

    registration

      let X be non empty set;

      let f,g be negative-yielding PartFunc of X, REAL ;

      cluster (f / g) -> positive-yielding;

      coherence

      proof

        let r be Real;

        set R = (f / g);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ (( dom g) \ (g " { 0 }))) by RFUNCT_1:def 1;

        then x in (( dom g) \ (g " { 0 })) by A1, XBOOLE_0:def 4;

        then

         A4: (g . x) in ( rng g) by FUNCT_1:def 3;

        x in ( dom f) by A1, A3, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x), b = (g . x) as negative Real by A4, Def2;

        (a * (b " )) is positive;

        hence thesis by A1, A2, RFUNCT_1:def 1;

      end;

    end

    registration

      let X be non empty set;

      let f be PartFunc of X, REAL ;

      cluster (f / f) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f / f);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) & (R . x) = r by FUNCT_1:def 3;

        ((f . x) * ((f . x) " )) is non negative;

        hence thesis by A1, RFUNCT_1:def 1;

      end;

    end

    registration

      let X be non empty set;

      let f,g be non-empty PartFunc of X, REAL ;

      cluster (f / g) -> non-empty;

      coherence

      proof

        set R = (f / g);

        assume not thesis;

        then 0 in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = 0 by FUNCT_1:def 3;

        

         A3: ( dom R) = (( dom f) /\ (( dom g) \ (g " { 0 }))) by RFUNCT_1:def 1;

        then x in (( dom g) \ (g " { 0 })) by A1, XBOOLE_0:def 4;

        then

         A4: (g . x) in ( rng g) by FUNCT_1:def 3;

        x in ( dom f) by A1, A3, XBOOLE_0:def 4;

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

        then

        reconsider a = (f . x), b = (g . x) as non zero Real by A4;

        (a * (b " )) is non zero;

        hence thesis by A1, A2, RFUNCT_1:def 1;

      end;

    end

    registration

      let X be set;

      let f be nonpositive-yielding Function of X, REAL ;

      cluster ( Inv f) -> nonpositive-yielding;

      coherence

      proof

        let r be Real;

        set R = ( Inv f);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        ( dom R) = X by FUNCT_2:def 1

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

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as non positive Real by Def3;

        (a " ) is non positive;

        hence thesis by A2, VALUED_1: 10;

      end;

    end

    registration

      let X be set;

      let f be nonnegative-yielding Function of X, REAL ;

      cluster ( Inv f) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        set R = ( Inv f);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        ( dom R) = X by FUNCT_2:def 1

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

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as non negative Real by Def4;

        (a " ) is non negative;

        hence thesis by A2, VALUED_1: 10;

      end;

    end

    registration

      let X be set;

      let f be positive-yielding Function of X, REAL ;

      cluster ( Inv f) -> positive-yielding;

      coherence

      proof

        let r be Real;

        set R = ( Inv f);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        ( dom R) = X by FUNCT_2:def 1

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

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as positive Real by Def1;

        (a " ) is positive;

        hence thesis by A2, VALUED_1: 10;

      end;

    end

    registration

      let X be set;

      let f be negative-yielding Function of X, REAL ;

      cluster ( Inv f) -> negative-yielding;

      coherence

      proof

        let r be Real;

        set R = ( Inv f);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        ( dom R) = X by FUNCT_2:def 1

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

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as negative Real by Def2;

        (a " ) is negative;

        hence thesis by A2, VALUED_1: 10;

      end;

    end

    registration

      let X be set;

      let f be non-empty Function of X, REAL ;

      cluster ( Inv f) -> non-empty;

      coherence

      proof

        set R = ( Inv f);

        assume not thesis;

        then 0 in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = 0 by FUNCT_1:def 3;

        ( dom R) = X by FUNCT_2:def 1

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

        then

        reconsider a = (f . x) as non zero Real by A1, ORDINAL1:def 16;

        (a " ) is non zero;

        hence thesis by A2, VALUED_1: 10;

      end;

    end

    registration

      let X be set;

      let f be non-empty Function of X, REAL ;

      cluster ( - f) -> non-empty;

      coherence ;

    end

    registration

      let X be set;

      let f be nonpositive-yielding Function of X, REAL ;

      cluster ( - f) -> nonnegative-yielding;

      coherence ;

    end

    registration

      let X be set;

      let f be nonnegative-yielding Function of X, REAL ;

      cluster ( - f) -> nonpositive-yielding;

      coherence ;

    end

    registration

      let X be set;

      let f be positive-yielding Function of X, REAL ;

      cluster ( - f) -> negative-yielding;

      coherence ;

    end

    registration

      let X be set;

      let f be negative-yielding Function of X, REAL ;

      cluster ( - f) -> positive-yielding;

      coherence ;

    end

    registration

      let X be set;

      let f be Function of X, REAL ;

      cluster ( abs f) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        set R = ( abs f);

        assume r in ( rng R);

        then

        consider x be object such that x in ( dom R) and

         A1: (R . x) = r by FUNCT_1:def 3;

         |.(f . x).| is non negative by COMPLEX1: 46;

        hence thesis by A1, VALUED_1: 18;

      end;

    end

    registration

      let X be set;

      let f be non-empty Function of X, REAL ;

      cluster ( abs f) -> positive-yielding;

      coherence

      proof

        let r be Real;

        set R = ( abs f);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        ( dom R) = ( dom f) by VALUED_1:def 11;

        then

        reconsider a = (f . x) as non zero Real by A1, ORDINAL1:def 16;

         |.a.| is positive by COMPLEX1: 47;

        hence thesis by A2, VALUED_1: 18;

      end;

    end

    registration

      let X be non empty set;

      let f be nonpositive-yielding Function of X, REAL ;

      cluster (f ^ ) -> nonpositive-yielding;

      coherence

      proof

        let r be Real;

        set R = (f ^ );

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        ( dom R) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

        then x in ( dom f) by A1, XBOOLE_0:def 5;

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

        then

        reconsider a = (f . x) as non positive Real by Def3;

        (a " ) is non positive;

        hence thesis by A1, A2, RFUNCT_1:def 2;

      end;

    end

    registration

      let X be non empty set;

      let f be nonnegative-yielding Function of X, REAL ;

      cluster (f ^ ) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f ^ );

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        ( dom R) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

        then x in ( dom f) by A1, XBOOLE_0:def 5;

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

        then

        reconsider a = (f . x) as non negative Real by Def4;

        (a " ) is non negative;

        hence thesis by A1, A2, RFUNCT_1:def 2;

      end;

    end

    registration

      let X be non empty set;

      let f be positive-yielding Function of X, REAL ;

      cluster (f ^ ) -> positive-yielding;

      coherence

      proof

        let r be Real;

        set R = (f ^ );

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        ( dom R) = ( dom f) by Th2;

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as positive Real by Def1;

        (a " ) is positive;

        hence thesis by A1, A2, RFUNCT_1:def 2;

      end;

    end

    registration

      let X be non empty set;

      let f be negative-yielding Function of X, REAL ;

      cluster (f ^ ) -> negative-yielding;

      coherence

      proof

        let r be Real;

        set R = (f ^ );

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        ( dom R) = ( dom f) by Th2;

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as negative Real by Def2;

        (a " ) is negative;

        hence thesis by A1, A2, RFUNCT_1:def 2;

      end;

    end

    registration

      let X be non empty set;

      let f be non-empty Function of X, REAL ;

      cluster (f ^ ) -> non-empty;

      coherence

      proof

        set R = (f ^ );

        assume not thesis;

        then 0 in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = 0 by FUNCT_1:def 3;

        ( dom R) = ( dom f) by Th2;

        then

        reconsider a = (f . x) as non zero Real by A1, ORDINAL1:def 16;

        (a " ) is non zero;

        hence thesis by A1, A2, RFUNCT_1:def 2;

      end;

    end

    definition

      let f be real-valued Function;

      :: PARTFUN3:def5

      func sqrt f -> Function means

      : Def5: ( dom it ) = ( dom f) & for x be object st x in ( dom it ) holds (it . x) = ( sqrt (f . x));

      existence

      proof

        deffunc F( object) = ( sqrt (f . $1));

        ex h be Function st ( dom h) = ( dom f) & for x be object st x in ( dom f) holds (h . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let h,g be Function such that

         A1: ( dom h) = ( dom f) and

         A2: for c be object st c in ( dom h) holds (h . c) = ( sqrt (f . c)) and

         A3: ( dom g) = ( dom f) and

         A4: for c be object st c in ( dom g) holds (g . c) = ( sqrt (f . c));

        now

          let x be object;

          assume

           A5: x in ( dom h);

          

          hence (h . x) = ( sqrt (f . x)) by A2

          .= (g . x) by A1, A3, A4, A5;

        end;

        hence thesis by A1, A3, FUNCT_1: 2;

      end;

    end

    registration

      let f be real-valued Function;

      cluster ( sqrt f) -> real-valued;

      coherence

      proof

        let x be object;

        set F = ( sqrt f);

        assume x in ( dom F);

        then (F . x) = ( sqrt (f . x)) by Def5;

        hence thesis;

      end;

    end

    definition

      let C be set, D be real-membered set, f be PartFunc of C, D;

      :: original: sqrt

      redefine

      func sqrt f -> PartFunc of C, REAL ;

      coherence

      proof

        set F = ( sqrt f);

        ( dom F) = ( dom f) & ( rng F) c= REAL by Def5, VALUED_0:def 3;

        hence thesis by RELSET_1: 4;

      end;

    end

    registration

      let X be set;

      let f be nonnegative-yielding Function of X, REAL ;

      cluster ( sqrt f) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        set R = ( sqrt f);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        ( dom R) = ( dom f) by Def5;

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as non negative Real by Def4;

        ( sqrt a) is non negative;

        hence thesis by A1, A2, Def5;

      end;

    end

    registration

      let X be set;

      let f be positive-yielding Function of X, REAL ;

      cluster ( sqrt f) -> positive-yielding;

      coherence

      proof

        let r be Real;

        set R = ( sqrt f);

        assume r in ( rng R);

        then

        consider x be object such that

         A1: x in ( dom R) and

         A2: (R . x) = r by FUNCT_1:def 3;

        ( dom R) = ( dom f) by Def5;

        then (f . x) in ( rng f) by A1, FUNCT_1:def 3;

        then

        reconsider a = (f . x) as positive Real by Def1;

        ( sqrt a) is positive;

        hence thesis by A1, A2, Def5;

      end;

    end

    definition

      let X be set, f be Function of X, REAL ;

      :: original: sqrt

      redefine

      func sqrt f -> Function of X, REAL ;

      coherence

      proof

        ( dom ( sqrt f)) = ( dom f) by Def5

        .= X by FUNCT_2:def 1;

        hence thesis by FUNCT_2:def 1;

      end;

    end

    definition

      let X be set, f be non-empty Function of X, REAL ;

      :: original: ^

      redefine

      func f ^ -> Function of X, REAL ;

      coherence

      proof

        ( dom (f ^ )) = ( dom f) by Th2

        .= X by FUNCT_2:def 1;

        hence thesis by FUNCT_2:def 1;

      end;

    end

    definition

      let X be non empty set, f be Function of X, REAL , g be non-empty Function of X, REAL ;

      :: original: /

      redefine

      func f / g -> Function of X, REAL ;

      coherence

      proof

        ( dom (f / g)) = (( dom f) /\ ( dom g)) by Th3

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

        .= (X /\ X) by FUNCT_2:def 1;

        hence thesis by FUNCT_2:def 1;

      end;

    end