PARTFUN3

:: On the Real Valued Functions
::  by Artur Korni{\l}owicz
::
:: Received December 10, 2004
:: Copyright (c) 2004-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, ARYTM_3, XXREAL_0, CARD_1, RELAT_1, SQUARE_1, FUNCT_1,
      TARSKI, XBOOLE_0, FUNCOP_1, ARYTM_1, SUBSET_1, VALUED_0, ORDINAL4,
      PARTFUN1, VALUED_1, XCMPLX_0, PRALG_1, COMPLEX1, MEMBERED, PARTFUN3,
      REAL_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, COMPLEX1, MEMBERED, SQUARE_1,
      RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, MEASURE6, VALUED_0,
      VALUED_1, RFUNCT_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1,
      FUNCOP_1;
 constructors REAL_1, SQUARE_1, COMPLEX1, RCOMP_1, RFUNCT_1, MEASURE6,
      FUNCOP_1, RELSET_1, NUMBERS;
 registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCOP_1, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, ORDINAL1;
 requirements NUMERALS, BOOLE, SUBSET, REAL;
 definitions RELAT_1, VALUED_0;
 equalities VALUED_1, ORDINAL1;
 expansions RELAT_1;
 theorems TARSKI, FUNCT_2, FUNCT_1, XBOOLE_0, FUNCOP_1, RFUNCT_1, SQUARE_1,
      XCMPLX_0, XREAL_1, COMPLEX1, VALUED_1, RELSET_1, XREAL_0;
 schemes FUNCT_1;

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
  for f being Function, A being 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 being 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;
    hence thesis by A2,TARSKI:def 1;
  end;
end;

definition
  let R be Relation;
  attr R is positive-yielding means
  :Def1:
  for r being Real st r in rng R holds 0 < r;
  attr R is negative-yielding means
  :Def2:
  for r being Real st r in rng R holds 0 > r;
  attr R is nonpositive-yielding means
  :Def3:
  for r being Real st r in rng R holds 0 >= r;
  attr R is nonnegative-yielding means
  :Def4:
  for r being 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 negative-yielding real-valued for Relation;
  existence
  proof
    take 1 --> -jj;
    thus thesis;
  end;
  cluster positive-yielding real-valued for Relation;
  existence
  proof
    take 1 --> jj;
    thus thesis;
  end;
end;

registration
  cluster negative-yielding real-valued for Function;
  existence
  proof
    take 1 --> -jj;
    thus thesis;
  end;
  cluster positive-yielding real-valued for Function;
  existence
  proof
    take 1 --> 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 Th2:
  for f being 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 Th3:
  for X being set, f being PartFunc of X,REAL,
  g being non-empty PartFunc of X,REAL holds dom(f/g) = dom f /\ dom g
proof
  let X be 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 f, g be nonpositive-yielding real-valued Function;
  cluster f+g -> nonpositive-yielding;
  coherence
  proof
    let r be Real;
    set R = f+g;
    assume r in rng R;
    then consider x being 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 f, g be nonnegative-yielding real-valued Function;
  cluster f+g -> nonnegative-yielding;
  coherence
  proof
    let r be Real;
    set R = f+g;
    assume r in rng R;
    then consider x being 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 f be positive-yielding real-valued Function;
  let g be nonnegative-yielding real-valued Function;
  cluster f+g -> positive-yielding;
  coherence
  proof
    let r be Real;
    set R = f+g;
    assume r in rng R;
    then consider x being 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 f be nonnegative-yielding real-valued Function;
  let g be positive-yielding real-valued Function;
  cluster f+g -> positive-yielding;
  coherence;
end;

registration
  let f be nonpositive-yielding real-valued Function;
  let g be negative-yielding real-valued Function;
  cluster f+g -> negative-yielding;
  coherence
  proof
    let r be Real;
    set R = f+g;
    assume r in rng R;
    then consider x being 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 f be negative-yielding real-valued Function;
  let g be nonpositive-yielding real-valued Function;
  cluster f+g -> negative-yielding;
  coherence;
end;

registration
  let f be nonnegative-yielding real-valued Function;
  let g be nonpositive-yielding real-valued Function;
  cluster f-g -> nonnegative-yielding;
  coherence
  proof
    let r be Real;
    set R = f-g;
    assume r in rng R;
    then consider x being 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 f be nonpositive-yielding real-valued Function;
  let g be nonnegative-yielding real-valued Function;
  cluster f-g -> nonpositive-yielding;
  coherence
  proof
    let r be Real;
    set R = f-g;
    assume r in rng R;
    then consider x being 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 f be positive-yielding real-valued Function;
  let g be nonpositive-yielding real-valued Function;
  cluster f-g -> positive-yielding;
  coherence
  proof
    let r be Real;
    set R = f-g;
    assume r in rng R;
    then consider x being 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 f be nonpositive-yielding real-valued Function;
  let g be positive-yielding real-valued Function;
  cluster f-g -> negative-yielding;
  coherence
  proof
    let r be Real;
    set R = f-g;
    assume r in rng R;
    then consider x being 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 f be negative-yielding real-valued Function;
  let g be nonnegative-yielding real-valued Function;
  cluster f-g -> negative-yielding;
  coherence
  proof
    let r be Real;
    set R = f-g;
    assume r in rng R;
    then consider x being 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 f be nonnegative-yielding real-valued Function;
  let g be negative-yielding real-valued Function;
  cluster f-g -> positive-yielding;
  coherence
  proof
    let r be Real;
    set R = f-g;
    assume r in rng R;
    then consider x being 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 f, g be nonpositive-yielding real-valued Function;
  cluster f(#)g -> nonnegative-yielding;
  coherence
  proof
    let r be Real;
    set R = f(#)g;
    assume r in rng R;
    then consider x being 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 f, g be nonnegative-yielding real-valued Function;
  cluster f(#)g -> nonnegative-yielding;
  coherence
  proof
    let r be Real;
    set R = f(#)g;
    assume r in rng R;
    then consider x being 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 f be nonpositive-yielding real-valued Function;
  let g be nonnegative-yielding real-valued Function;
  cluster f(#)g -> nonpositive-yielding;
  coherence
  proof
    let r be Real;
    set R = f(#)g;
    assume r in rng R;
    then consider x being 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 f be nonnegative-yielding real-valued Function;
  let g be nonpositive-yielding real-valued Function;
  cluster f(#)g -> nonpositive-yielding;
  coherence;
end;

registration
  let f be positive-yielding real-valued Function;
  let g be negative-yielding real-valued Function;
  cluster f(#)g -> negative-yielding;
  coherence
  proof
    let r be Real;
    set R = f(#)g;
    assume r in rng R;
    then consider x being 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 f be negative-yielding real-valued Function;
  let g be positive-yielding real-valued Function;
  cluster f(#)g -> negative-yielding;
  coherence;
end;

registration
  let f, g be positive-yielding real-valued Function;
  cluster f(#)g -> positive-yielding;
  coherence
  proof
    let r be Real;
    set R = f(#)g;
    assume r in rng R;
    then consider x being 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 f, g be negative-yielding real-valued Function;
  cluster f(#)g -> positive-yielding;
  coherence
  proof
    let r be Real;
    set R = f(#)g;
    assume r in rng R;
    then consider x being 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 f, g be non-empty real-valued Function;
  cluster f(#)g -> non-empty;
  coherence
  proof
    set R = f(#)g;
    assume not thesis;
    then consider x being 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 f be real-valued Function;
  cluster f(#)f -> nonnegative-yielding;
  coherence
  proof
    let r be Real;
    set R = f(#)f;
    assume r in rng R;
    then consider x being 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 r be non positive Real;
  let f be nonpositive-yielding real-valued Function;
  cluster r(#)f -> nonnegative-yielding;
  coherence
  proof
    let z be Real;
    set R = r(#)f;
    assume z in rng R;
    then consider x being 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 r be non negative Real;
  let f be nonnegative-yielding real-valued Function;
  cluster r(#)f -> nonnegative-yielding;
  coherence
  proof
    let z be Real;
    set R = r(#)f;
    assume z in rng R;
    then consider x being 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 r be non positive Real;
  let f be nonnegative-yielding real-valued Function;
  cluster r(#)f -> nonpositive-yielding;
  coherence
  proof
    let z be Real;
    set R = r(#)f;
    assume z in rng R;
    then consider x being 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 r be non negative Real;
  let f be nonpositive-yielding real-valued Function;
  cluster r(#)f -> nonpositive-yielding;
  coherence
  proof
    let z be Real;
    set R = r(#)f;
    assume z in rng R;
    then consider x being 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 r be positive Real;
  let f be negative-yielding real-valued Function;
  cluster r(#)f -> negative-yielding;
  coherence
  proof
    let z be Real;
    set R = r(#)f;
    assume z in rng R;
    then consider x being 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 r be negative Real;
  let f be positive-yielding real-valued Function;
  cluster r(#)f -> negative-yielding;
  coherence
  proof
    let z be Real;
    set R = r(#)f;
    assume z in rng R;
    then consider x being 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 r be positive Real;
  let f be positive-yielding real-valued Function;
  cluster r(#)f -> positive-yielding;
  coherence
  proof
    let z be Real;
    set R = r(#)f;
    assume z in rng R;
    then consider x being 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 r be negative Real;
  let f be negative-yielding real-valued Function;
  cluster r(#)f -> positive-yielding;
  coherence
  proof
    let z be Real;
    set R = r(#)f;
    assume z in rng R;
    then consider x being 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 r be non zero Real;
  let f be non-empty real-valued Function;
  cluster r(#)f -> non-empty;
  coherence
  proof
    set R = r(#)f;
    assume not thesis;
    then consider x being 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 f, g be nonpositive-yielding real-valued Function;
  cluster f/g -> nonnegative-yielding;
  coherence
  proof
    let r be Real;
    set R = f/g;
    assume r in rng R;
    then consider x being 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
A4: g.x in rng g by A1,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 f, g be nonnegative-yielding real-valued Function;
  cluster f/g -> nonnegative-yielding;
  coherence
  proof
    let r be Real;
    set R = f/g;
    assume r in rng R;
    then consider x being 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
A4: g.x in rng g by A1,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 f be nonpositive-yielding real-valued Function;
  let g be nonnegative-yielding real-valued Function;
  cluster f/g -> nonpositive-yielding;
  coherence
  proof
    let r be Real;
    set R = f/g;
    assume r in rng R;
    then consider x being 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;
    g.x in rng g by A1,A3,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 f be nonnegative-yielding real-valued Function;
  let g be nonpositive-yielding real-valued Function;
  cluster f/g -> nonpositive-yielding;
  coherence
  proof
    let r be Real;
    set R = f/g;
    assume r in rng R;
    then consider x being 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;
    g.x in rng g by A1,A3,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 f be positive-yielding real-valued Function;
  let g be negative-yielding real-valued Function;
  cluster f/g -> negative-yielding;
  coherence
  proof
    let r be Real;
    set R = f/g;
    assume r in rng R;
    then consider x being 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;
    g.x in rng g by A1,A3,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 f be negative-yielding real-valued Function;
  let g be positive-yielding real-valued Function;
  cluster f/g -> negative-yielding;
  coherence
  proof
    let r be Real;
    set R = f/g;
    assume r in rng R;
    then consider x being 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;
    g.x in rng g by A1,A3,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 f, g be positive-yielding real-valued Function;
  cluster f/g -> positive-yielding;
  coherence
  proof
    let r be Real;
    set R = f/g;
    assume r in rng R;
    then consider x being 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
A4: g.x in rng g by A1,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 f, g be negative-yielding real-valued Function;
  cluster f/g -> positive-yielding;
  coherence
  proof
    let r be Real;
    set R = f/g;
    assume r in rng R;
    then consider x being 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
A4: g.x in rng g by A1,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 f be real-valued Function;
  cluster f/f -> nonnegative-yielding;
  coherence
  proof
    let r be Real;
    set R = f/f;
    assume r in rng R;
    then consider x being 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 f, g be non-empty real-valued Function;
  cluster f/g -> non-empty;
  coherence
  proof
    set R = f/g;
    assume not thesis;
    then consider x being 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
A4: g.x in rng g by A1,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 f be nonpositive-yielding real-valued Function;
  cluster Inv f -> nonpositive-yielding;
  coherence
  proof
    let r be Real;
    set R = Inv f;
    assume r in rng R;
    then consider x being 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 7;
    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 f be nonnegative-yielding real-valued Function;
  cluster Inv f -> nonnegative-yielding;
  coherence
  proof
    let r be Real;
    set R = Inv f;
    assume r in rng R;
    then consider x being 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 7;
    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 f be positive-yielding real-valued Function;
  cluster Inv f -> positive-yielding;
  coherence
  proof
    let r be Real;
    set R = Inv f;
    assume r in rng R;
    then consider x being 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 7;
    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 f be negative-yielding real-valued Function;
  cluster Inv f -> negative-yielding;
  coherence
  proof
    let r be Real;
    set R = Inv f;
    assume r in rng R;
    then consider x being 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 7;
    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 f be non-empty real-valued Function;
  cluster Inv f -> non-empty;
  coherence
  proof
    set R = Inv f;
    assume not thesis;
    then consider x being 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 7;
    then f.x in rng f by A1,FUNCT_1:def 3;
    then reconsider a = f.x as non zero Real;
    a" is non zero;
    hence thesis by A2,VALUED_1:10;
  end;
end;

registration
  let f be non-empty real-valued Function;
  cluster -f -> non-empty;
  coherence;
end;

registration
  let f be nonpositive-yielding real-valued Function;
  cluster -f -> nonnegative-yielding;
  coherence;
end;

registration
  let f be nonnegative-yielding real-valued Function;
  cluster -f -> nonpositive-yielding;
  coherence;
end;

registration
  let f be positive-yielding real-valued Function;
  cluster -f -> negative-yielding;
  coherence;
end;

registration
  let f be negative-yielding real-valued Function;
  cluster -f -> positive-yielding;
  coherence;
end;

registration
  let f be real-valued Function;
  cluster abs f -> nonnegative-yielding;
  coherence
  proof
    let r be Real;
    set R = abs f;
    assume r in rng R;
    then consider x being 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 f be non-empty real-valued Function;
  cluster abs f -> positive-yielding;
  coherence
  proof
    let r be Real;
    set R = abs f;
    assume r in rng R;
    then consider x being 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 f.x in rng f by A1,FUNCT_1:def 3;
    then reconsider a = f.x as non zero Real;
    |.a.| is positive by COMPLEX1:47;
    hence thesis by A2,VALUED_1:18;
  end;
end;

registration
  let f be nonpositive-yielding real-valued Function;
  cluster f^ -> nonpositive-yielding;
  coherence
  proof
    let r be Real;
    set R = f^;
    assume r in rng R;
    then consider x being 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 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 A1,A2,RFUNCT_1:def 2;
  end;
end;

registration
  let f be nonnegative-yielding real-valued Function;
  cluster f^ -> nonnegative-yielding;
  coherence
  proof
    let r be Real;
    set R = f^;
    assume r in rng R;
    then consider x being 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 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 A1,A2,RFUNCT_1:def 2;
  end;
end;

registration
  let f be positive-yielding real-valued Function;
  cluster f^ -> positive-yielding;
  coherence
  proof
    let r be Real;
    set R = f^;
    assume r in rng R;
    then consider x being 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 f be negative-yielding real-valued Function;
  cluster f^ -> negative-yielding;
  coherence
  proof
    let r be Real;
    set R = f^;
    assume r in rng R;
    then consider x being 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 f be non-empty real-valued Function;
  cluster f^ -> non-empty;
  coherence
  proof
    set R = f^;
    assume not thesis;
    then consider x being 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 f.x in rng f by A1,FUNCT_1:def 3;
    then reconsider a = f.x as non zero Real;
    a" is non zero;
    hence thesis by A1,A2,RFUNCT_1:def 2;
  end;
end;

definition
  let f be real-valued Function;
  func sqrt f -> Function means
  :Def5:
  dom it = dom f & for x being object st x in dom it holds it.x = sqrt(f.x);
  existence
  proof
    deffunc F(object) = sqrt (f.$1);
    ex h being Function st dom h = dom f & for x being 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 being object st c in dom h holds h.c = sqrt (f.c) and
A3: dom g = dom f and
A4: for c being 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;
  redefine func sqrt f -> PartFunc of C,REAL;  :: redefines sqrt (PARTFUN3, definition)
  coherence
  proof
    dom sqrt f = dom f & rng sqrt f c= REAL by Def5;
    hence thesis by RELSET_1:4;
  end;
end;

registration
  let f be nonnegative-yielding real-valued Function;
  cluster sqrt f -> nonnegative-yielding;
  coherence
  proof
    let r be Real;
    set R = sqrt f;
    assume r in rng R;
    then consider x being 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 f be positive-yielding real-valued Function;
  cluster sqrt f -> positive-yielding;
  coherence
  proof
    let r be Real;
    set R = sqrt f;
    assume r in rng R;
    then consider x being 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;
  redefine func sqrt f -> Function of X,REAL;  :: redefines sqrt (PARTFUN3, definition)
  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;
  redefine func f^ -> Function of X,REAL;  :: redefines ^ (RFUNCT_1, definition)
  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 set;
  let f be Function of X,REAL;
  let g be non-empty Function of X,REAL;
  redefine func f/g -> Function of X,REAL;  :: redefines / (RFUNCT_1, definition)
  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;