:: PARTFUN3 semantic presentation

begin

registration
let r be real number ;
clusterr / r ->  non negative ;
coherence
 not r / r is negative
proof
 ( r <= 0 or 0 <= r ) ;
hence  not r / r is negative ; ::_thesis: verum
end;
end;

registration
let r be real number ;
clusterr * r ->  non negative ;
coherence
 not r * r is negative by XREAL_1:63;
clusterr * (r ") ->  non negative ;
coherence
 not r * (r ") is negative
proof
 r * (r ") = r / r by XCMPLX_0:def_9;
hence  not r * (r ") is negative ; ::_thesis: verum
end;
end;

registration
let r be real non negative number ;
cluster sqrt r ->  non negative ;
coherence
 not sqrt r is negative by SQUARE_1:def_2;
end;

registration
let r be real positive number ;
cluster sqrt r ->  positive ;
coherence
 sqrt r is positive by SQUARE_1:25;
end;

theorem :: PARTFUN3:1
for f being Function
for A being set st f is one-to-one & A c= dom (f ") holds
f .: ((f ") .: A) = A
proof
let f be Function; ::_thesis: for A being set st f is one-to-one & A c= dom (f ") holds
f .: ((f ") .: A) = A
let A be set ; ::_thesis: ( f is one-to-one & A c= dom (f ") implies f .: ((f ") .: A) = A )
assume that
A1: f is one-to-one and
A2: A c= dom (f ") ; ::_thesis: f .: ((f ") .: A) = A
 ((f ") ") .: ((f ") .: A) = A by A1, A2, FUNCT_1:107;
hence  f .: ((f ") .: A) = A by A1, FUNCT_1:43; ::_thesis: verum
end;

registration
let f be non-empty Function;
clusterf " {0} ->  empty ;
coherence
 f " {0} is empty
proof
assume  not f " {0} is empty ; ::_thesis: contradiction
then consider x being set  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  contradiction by A2, RELAT_1:def_9; ::_thesis: verum
end;
end;

definition
let R be Relation;
attrR is positive-yielding  means :Def1: :: PARTFUN3:def 1
 for r being real number st r in rng R holds
0 < r;
attrR is negative-yielding  means :Def2: :: PARTFUN3:def 2
 for r being real number st r in rng R holds
0 > r;
attrR is nonpositive-yielding  means :Def3: :: PARTFUN3:def 3
 for r being real number st r in rng R holds
0 >= r;
attrR is nonnegative-yielding  means :Def4: :: PARTFUN3:def 4
 for r being real number st r in rng R holds
0 <= r;
end;

:: deftheorem Def1 defines positive-yielding PARTFUN3:def_1_:_
 for R being Relation holds
( R is positive-yielding iff for r being real number st r in rng R holds
0 < r );

:: deftheorem Def2 defines negative-yielding PARTFUN3:def_2_:_
 for R being Relation holds
( R is negative-yielding iff for r being real number st r in rng R holds
0 > r );

:: deftheorem Def3 defines nonpositive-yielding PARTFUN3:def_3_:_
 for R being Relation holds
( R is nonpositive-yielding iff for r being real number st r in rng R holds
0 >= r );

:: deftheorem Def4 defines nonnegative-yielding PARTFUN3:def_4_:_
 for R being Relation holds
( R is nonnegative-yielding iff for r being real number st r in rng R holds
0 <= r );

registration
let X be set ;
let r be real positive number ;
clusterX --> r ->  positive-yielding ;
coherence
 X --> r is positive-yielding
proof
let x be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( x in rng (X --> r) implies 0 < x )
assume  x in rng (X --> r) ; ::_thesis: 0 < x
hence  0 < x by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let X be set ;
let r be real negative number ;
clusterX --> r ->  negative-yielding ;
coherence
 X --> r is negative-yielding
proof
let x be real number ; :: according to PARTFUN3:def_2 ::_thesis: ( x in rng (X --> r) implies 0 > x )
assume  x in rng (X --> r) ; ::_thesis: 0 > x
hence  0 > x by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let X be set ;
let r be real non positive number ;
clusterX --> r ->  nonpositive-yielding ;
coherence
 X --> r is nonpositive-yielding
proof
let x be real number ; :: according to PARTFUN3:def_3 ::_thesis: ( x in rng (X --> r) implies 0 >= x )
assume  x in rng (X --> r) ; ::_thesis: 0 >= x
hence  0 >= x by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let X be set ;
let r be real non negative number ;
clusterX --> r ->  nonnegative-yielding ;
coherence
 X --> r is nonnegative-yielding
proof
let x be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( x in rng (X --> r) implies 0 <= x )
assume  x in rng (X --> r) ; ::_thesis: 0 <= x
hence  0 <= x by TARSKI:def_1; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
clusterX --> 0 ->  non non-empty ;
coherence
 not X --> 0 is non-empty
proof
 rng (X --> 0) = {0} by FUNCOP_1:8;
hence  {} in rng (X --> 0) by TARSKI:def_1; :: according to RELAT_1:def_9 ::_thesis: verum
end;
end;

registration
cluster Relation-like positive-yielding  ->  non-empty nonnegative-yielding for set ;
coherence
 for b1 being Relation st b1 is positive-yielding holds
( b1 is nonnegative-yielding & b1 is non-empty )
proof
let R be Relation; ::_thesis: ( R is positive-yielding implies ( R is nonnegative-yielding & R is non-empty ) )
assume A1: for r being real number st r in rng R holds
0 < r ; :: according to PARTFUN3:def_1 ::_thesis: ( R is nonnegative-yielding & R is non-empty )
thus  R is nonnegative-yielding ::_thesis: R is non-empty
proof
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( r in rng R implies 0 <= r )
thus  ( r in rng R implies 0 <= r ) by A1; ::_thesis: verum
end;
assume  not R is non-empty ; ::_thesis: contradiction
then  0 in rng R by RELAT_1:def_9;
hence  contradiction by A1; ::_thesis: verum
end;
cluster Relation-like negative-yielding  ->  non-empty nonpositive-yielding for set ;
coherence
 for b1 being Relation st b1 is negative-yielding holds
( b1 is nonpositive-yielding & b1 is non-empty )
proof
let R be Relation; ::_thesis: ( R is negative-yielding implies ( R is nonpositive-yielding & R is non-empty ) )
assume A2: for r being real number st r in rng R holds
0 > r ; :: according to PARTFUN3:def_2 ::_thesis: ( R is nonpositive-yielding & R is non-empty )
thus  R is nonpositive-yielding ::_thesis: R is non-empty
proof
let r be real number ; :: according to PARTFUN3:def_3 ::_thesis: ( r in rng R implies 0 >= r )
thus  ( r in rng R implies 0 >= r ) by A2; ::_thesis: verum
end;
assume  not R is non-empty ; ::_thesis: contradiction
then  0 in rng R by RELAT_1:def_9;
hence  contradiction by A2; ::_thesis: verum
end;
end;

registration
let X be set ;
cluster Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued negative-yielding for Element of K6(K7(X,REAL));
existence
 ex b1 being Function of X,REAL st b1 is negative-yielding
proof
take  X --> (- 1) ; ::_thesis: X --> (- 1) is negative-yielding
thus  X --> (- 1) is negative-yielding ; ::_thesis: verum
end;
cluster Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued positive-yielding for Element of K6(K7(X,REAL));
existence
 ex b1 being Function of X,REAL st b1 is positive-yielding
proof
take  X --> 1 ; ::_thesis: X --> 1 is positive-yielding
thus  X --> 1 is positive-yielding ; ::_thesis: verum
end;
end;

registration
cluster Relation-like non-empty Function-like real-valued for set ;
existence
 ex b1 being Function st
( b1 is non-empty & b1 is real-valued )
proof
set f = the non-empty Function of 0,REAL;
take  the non-empty Function of 0,REAL ; ::_thesis: ( the non-empty Function of 0,REAL is non-empty & the non-empty Function of 0,REAL is real-valued )
thus  ( the non-empty Function of 0,REAL is non-empty & the non-empty Function of 0,REAL is real-valued ) ; ::_thesis: verum
end;
end;

theorem Th2: :: PARTFUN3:2
for f being non-empty real-valued Function holds dom (f ^) = dom f
proof
let f be non-empty real-valued Function; ::_thesis: dom (f ^) = dom f
thus  dom (f ^) = (dom f) \ (f " {0}) by RFUNCT_1:def_2
.= dom f ; ::_thesis: verum
end;

theorem Th3: :: PARTFUN3:3
for X being non empty set
for f being PartFunc of X,REAL
for g being non-empty PartFunc of X,REAL holds dom (f / g) = (dom f) /\ (dom g)
proof
let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL
for g being non-empty PartFunc of X,REAL holds dom (f / g) = (dom f) /\ (dom g)
let f be PartFunc of X,REAL; ::_thesis: for g being non-empty PartFunc of X,REAL holds dom (f / g) = (dom f) /\ (dom g)
let g be non-empty PartFunc of X,REAL; ::_thesis: dom (f / g) = (dom f) /\ (dom g)
thus  dom (f / g) = (dom f) /\ ((dom g) \ (g " {0})) by RFUNCT_1:def_1
.= (dom f) /\ (dom g) ; ::_thesis: verum
end;

registration
let X be set ;
let f, g be nonpositive-yielding PartFunc of X,REAL;
clusterf + g ->  nonpositive-yielding ;
coherence
 f + g is nonpositive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_3 ::_thesis: ( r in rng (f + g) implies 0 >= r )
set R = f + g;
assume  r in rng (f + g) ; ::_thesis: 0 >= r
then consider x being set  such that
A1: x in dom (f + g) and
A2: (f + g) . x = r by FUNCT_1:def_3;
A3: dom (f + g) = (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 real non positive number by A4, Def3;
 not a + b is positive ;
hence  0 >= r by A1, A2, VALUED_1:def_1; ::_thesis: verum
end;
end;

registration
let X be set ;
let f, g be nonnegative-yielding PartFunc of X,REAL;
clusterf + g ->  nonnegative-yielding ;
coherence
 f + g is nonnegative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( r in rng (f + g) implies 0 <= r )
set R = f + g;
assume  r in rng (f + g) ; ::_thesis: 0 <= r
then consider x being set  such that
A1: x in dom (f + g) and
A2: (f + g) . x = r by FUNCT_1:def_3;
A3: dom (f + g) = (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 real non negative number by A4, Def4;
 not a + b is negative ;
hence  0 <= r by A1, A2, VALUED_1:def_1; ::_thesis: verum
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;
clusterf + g ->  positive-yielding ;
coherence
 f + g is positive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( r in rng (f + g) implies 0 < r )
set R = f + g;
assume  r in rng (f + g) ; ::_thesis: 0 < r
then consider x being set  such that
A1: x in dom (f + g) and
A2: (f + g) . x = r by FUNCT_1:def_3;
A3: dom (f + g) = (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 real positive number 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 real non negative number by Def4;
 a + b is positive ;
hence  0 < r by A1, A2, VALUED_1:def_1; ::_thesis: verum
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;
clusterf + g ->  positive-yielding ;
coherence
 f + g is positive-yielding ;
end;

registration
let X be set ;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be negative-yielding PartFunc of X,REAL;
clusterf + g ->  negative-yielding ;
coherence
 f + g is negative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_2 ::_thesis: ( r in rng (f + g) implies 0 > r )
set R = f + g;
assume  r in rng (f + g) ; ::_thesis: 0 > r
then consider x being set  such that
A1: x in dom (f + g) and
A2: (f + g) . x = r by FUNCT_1:def_3;
A3: dom (f + g) = (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 real non positive number 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 real negative number by Def2;
 a + b is negative ;
hence  0 > r by A1, A2, VALUED_1:def_1; ::_thesis: verum
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;
clusterf + g ->  negative-yielding ;
coherence
 f + g is negative-yielding ;
end;

registration
let X be set ;
let f be nonnegative-yielding PartFunc of X,REAL;
let g be nonpositive-yielding PartFunc of X,REAL;
clusterf - g ->  nonnegative-yielding ;
coherence
 f - g is nonnegative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( r in rng (f - g) implies 0 <= r )
set R = f - g;
assume  r in rng (f - g) ; ::_thesis: 0 <= r
then consider x being set  such that
A1: x in dom (f - g) and
A2: (f - g) . x = r by FUNCT_1:def_3;
A3: dom (f - g) = (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 real non negative number 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 real non positive number by Def3;
 not a - b is negative ;
hence  0 <= r by A1, A2, VALUED_1:13; ::_thesis: verum
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;
clusterf - g ->  nonpositive-yielding ;
coherence
 f - g is nonpositive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_3 ::_thesis: ( r in rng (f - g) implies 0 >= r )
set R = f - g;
assume  r in rng (f - g) ; ::_thesis: 0 >= r
then consider x being set  such that
A1: x in dom (f - g) and
A2: (f - g) . x = r by FUNCT_1:def_3;
A3: dom (f - g) = (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 real non positive number 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 real non negative number by Def4;
 not a - b is positive ;
hence  0 >= r by A1, A2, VALUED_1:13; ::_thesis: verum
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;
clusterf - g ->  positive-yielding ;
coherence
 f - g is positive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( r in rng (f - g) implies 0 < r )
set R = f - g;
assume  r in rng (f - g) ; ::_thesis: 0 < r
then consider x being set  such that
A1: x in dom (f - g) and
A2: (f - g) . x = r by FUNCT_1:def_3;
A3: dom (f - g) = (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 real positive number 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 real non positive number by Def3;
 a - b is positive ;
hence  0 < r by A1, A2, VALUED_1:13; ::_thesis: verum
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;
clusterf - g ->  negative-yielding ;
coherence
 f - g is negative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_2 ::_thesis: ( r in rng (f - g) implies 0 > r )
set R = f - g;
assume  r in rng (f - g) ; ::_thesis: 0 > r
then consider x being set  such that
A1: x in dom (f - g) and
A2: (f - g) . x = r by FUNCT_1:def_3;
A3: dom (f - g) = (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 real non positive number 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 real positive number by Def1;
 a - b is negative ;
hence  0 > r by A1, A2, VALUED_1:13; ::_thesis: verum
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;
clusterf - g ->  negative-yielding ;
coherence
 f - g is negative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_2 ::_thesis: ( r in rng (f - g) implies 0 > r )
set R = f - g;
assume  r in rng (f - g) ; ::_thesis: 0 > r
then consider x being set  such that
A1: x in dom (f - g) and
A2: (f - g) . x = r by FUNCT_1:def_3;
A3: dom (f - g) = (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 real negative number 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 real non negative number by Def4;
 a - b is negative ;
hence  0 > r by A1, A2, VALUED_1:13; ::_thesis: verum
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;
clusterf - g ->  positive-yielding ;
coherence
 f - g is positive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( r in rng (f - g) implies 0 < r )
set R = f - g;
assume  r in rng (f - g) ; ::_thesis: 0 < r
then consider x being set  such that
A1: x in dom (f - g) and
A2: (f - g) . x = r by FUNCT_1:def_3;
A3: dom (f - g) = (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 real non negative number 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 real negative number by Def2;
 a - b is positive ;
hence  0 < r by A1, A2, VALUED_1:13; ::_thesis: verum
end;
end;

registration
let X be set ;
let f, g be nonpositive-yielding PartFunc of X,REAL;
clusterf (#) g ->  nonnegative-yielding ;
coherence
 f (#) g is nonnegative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( r in rng (f (#) g) implies 0 <= r )
set R = f (#) g;
assume  r in rng (f (#) g) ; ::_thesis: 0 <= r
then consider x being set  such that
A1: x in dom (f (#) g) and
A2: (f (#) g) . x = r by FUNCT_1:def_3;
A3: dom (f (#) g) = (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 real non positive number by A4, Def3;
 not a * b is negative ;
hence  0 <= r by A2, VALUED_1:5; ::_thesis: verum
end;
end;

registration
let X be set ;
let f, g be nonnegative-yielding PartFunc of X,REAL;
clusterf (#) g ->  nonnegative-yielding ;
coherence
 f (#) g is nonnegative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( r in rng (f (#) g) implies 0 <= r )
set R = f (#) g;
assume  r in rng (f (#) g) ; ::_thesis: 0 <= r
then consider x being set  such that
A1: x in dom (f (#) g) and
A2: (f (#) g) . x = r by FUNCT_1:def_3;
A3: dom (f (#) g) = (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 real non negative number by A4, Def4;
 not a * b is negative ;
hence  0 <= r by A2, VALUED_1:5; ::_thesis: verum
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;
clusterf (#) g ->  nonpositive-yielding ;
coherence
 f (#) g is nonpositive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_3 ::_thesis: ( r in rng (f (#) g) implies 0 >= r )
set R = f (#) g;
assume  r in rng (f (#) g) ; ::_thesis: 0 >= r
then consider x being set  such that
A1: x in dom (f (#) g) and
A2: (f (#) g) . x = r by FUNCT_1:def_3;
A3: dom (f (#) g) = (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 real non positive number 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 real non negative number by Def4;
 not a * b is positive ;
hence  0 >= r by A2, VALUED_1:5; ::_thesis: verum
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;
clusterf (#) g ->  nonpositive-yielding ;
coherence
 f (#) g is nonpositive-yielding ;
end;

registration
let X be set ;
let f be positive-yielding PartFunc of X,REAL;
let g be negative-yielding PartFunc of X,REAL;
clusterf (#) g ->  negative-yielding ;
coherence
 f (#) g is negative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_2 ::_thesis: ( r in rng (f (#) g) implies 0 > r )
set R = f (#) g;
assume  r in rng (f (#) g) ; ::_thesis: 0 > r
then consider x being set  such that
A1: x in dom (f (#) g) and
A2: (f (#) g) . x = r by FUNCT_1:def_3;
A3: dom (f (#) g) = (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 real positive number 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 real negative number by Def2;
 a * b is negative ;
hence  0 > r by A2, VALUED_1:5; ::_thesis: verum
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;
clusterf (#) g ->  negative-yielding ;
coherence
 f (#) g is negative-yielding ;
end;

registration
let X be set ;
let f, g be positive-yielding PartFunc of X,REAL;
clusterf (#) g ->  positive-yielding ;
coherence
 f (#) g is positive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( r in rng (f (#) g) implies 0 < r )
set R = f (#) g;
assume  r in rng (f (#) g) ; ::_thesis: 0 < r
then consider x being set  such that
A1: x in dom (f (#) g) and
A2: (f (#) g) . x = r by FUNCT_1:def_3;
A3: dom (f (#) g) = (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 real positive number by A4, Def1;
 a * b is positive ;
hence  0 < r by A2, VALUED_1:5; ::_thesis: verum
end;
end;

registration
let X be set ;
let f, g be negative-yielding PartFunc of X,REAL;
clusterf (#) g ->  positive-yielding ;
coherence
 f (#) g is positive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( r in rng (f (#) g) implies 0 < r )
set R = f (#) g;
assume  r in rng (f (#) g) ; ::_thesis: 0 < r
then consider x being set  such that
A1: x in dom (f (#) g) and
A2: (f (#) g) . x = r by FUNCT_1:def_3;
A3: dom (f (#) g) = (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 real negative number by A4, Def2;
 a * b is positive ;
hence  0 < r by A2, VALUED_1:5; ::_thesis: verum
end;
end;

registration
let X be set ;
let f, g be non-empty PartFunc of X,REAL;
clusterf (#) g ->  non-empty ;
coherence
 f (#) g is non-empty
proof
set R = f (#) g;
assume  not f (#) g is non-empty ; ::_thesis: contradiction
then  0 in rng (f (#) g) by RELAT_1:def_9;
then consider x being set  such that
A1: x in dom (f (#) g) and
A2: (f (#) g) . x = 0 by FUNCT_1:def_3;
A3: dom (f (#) g) = (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 number by A4, RELAT_1:def_9;
 not a * b is zero ;
hence  contradiction by A2, VALUED_1:5; ::_thesis: verum
end;
end;

registration
let X be set ;
let f be PartFunc of X,REAL;
clusterf (#) f ->  nonnegative-yielding ;
coherence
 f (#) f is nonnegative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( r in rng (f (#) f) implies 0 <= r )
set R = f (#) f;
assume  r in rng (f (#) f) ; ::_thesis: 0 <= r
then consider x being set  such that
 x in dom (f (#) f) and
A1: (f (#) f) . x = r by FUNCT_1:def_3;
 not (f . x) * (f . x) is negative ;
hence  0 <= r by A1, VALUED_1:5; ::_thesis: verum
end;
end;

registration
let X be set ;
let r be real non positive number ;
let f be nonpositive-yielding PartFunc of X,REAL;
clusterr (#) f ->  nonnegative-yielding ;
coherence
 r (#) f is nonnegative-yielding
proof
let z be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( z in rng (r (#) f) implies 0 <= z )
set R = r (#) f;
assume  z in rng (r (#) f) ; ::_thesis: 0 <= z
then consider x being set  such that
A1: x in dom (r (#) f) and
A2: (r (#) f) . x = z by FUNCT_1:def_3;
 dom (r (#) f) = 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 real non positive number by Def3;
 not r * a is negative ;
hence  0 <= z by A1, A2, VALUED_1:def_5; ::_thesis: verum
end;
end;

registration
let X be set ;
let r be real non negative number ;
let f be nonnegative-yielding PartFunc of X,REAL;
clusterr (#) f ->  nonnegative-yielding ;
coherence
 r (#) f is nonnegative-yielding
proof
let z be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( z in rng (r (#) f) implies 0 <= z )
set R = r (#) f;
assume  z in rng (r (#) f) ; ::_thesis: 0 <= z
then consider x being set  such that
A1: x in dom (r (#) f) and
A2: (r (#) f) . x = z by FUNCT_1:def_3;
 dom (r (#) f) = 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 real non negative number by Def4;
 not r * a is negative ;
hence  0 <= z by A1, A2, VALUED_1:def_5; ::_thesis: verum
end;
end;

registration
let X be set ;
let r be real non positive number ;
let f be nonnegative-yielding PartFunc of X,REAL;
clusterr (#) f ->  nonpositive-yielding ;
coherence
 r (#) f is nonpositive-yielding
proof
let z be real number ; :: according to PARTFUN3:def_3 ::_thesis: ( z in rng (r (#) f) implies 0 >= z )
set R = r (#) f;
assume  z in rng (r (#) f) ; ::_thesis: 0 >= z
then consider x being set  such that
A1: x in dom (r (#) f) and
A2: (r (#) f) . x = z by FUNCT_1:def_3;
 dom (r (#) f) = 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 real non negative number by Def4;
 not r * a is positive ;
hence  0 >= z by A1, A2, VALUED_1:def_5; ::_thesis: verum
end;
end;

registration
let X be set ;
let r be real non negative number ;
let f be nonpositive-yielding PartFunc of X,REAL;
clusterr (#) f ->  nonpositive-yielding ;
coherence
 r (#) f is nonpositive-yielding
proof
let z be real number ; :: according to PARTFUN3:def_3 ::_thesis: ( z in rng (r (#) f) implies 0 >= z )
set R = r (#) f;
assume  z in rng (r (#) f) ; ::_thesis: 0 >= z
then consider x being set  such that
A1: x in dom (r (#) f) and
A2: (r (#) f) . x = z by FUNCT_1:def_3;
 dom (r (#) f) = 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 real non positive number by Def3;
 not r * a is positive ;
hence  0 >= z by A1, A2, VALUED_1:def_5; ::_thesis: verum
end;
end;

registration
let X be set ;
let r be real positive number ;
let f be negative-yielding PartFunc of X,REAL;
clusterr (#) f ->  negative-yielding ;
coherence
 r (#) f is negative-yielding
proof
let z be real number ; :: according to PARTFUN3:def_2 ::_thesis: ( z in rng (r (#) f) implies 0 > z )
set R = r (#) f;
assume  z in rng (r (#) f) ; ::_thesis: 0 > z
then consider x being set  such that
A1: x in dom (r (#) f) and
A2: (r (#) f) . x = z by FUNCT_1:def_3;
 dom (r (#) f) = 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 real negative number by Def2;
 r * a is negative ;
hence  0 > z by A1, A2, VALUED_1:def_5; ::_thesis: verum
end;
end;

registration
let X be set ;
let r be real negative number ;
let f be positive-yielding PartFunc of X,REAL;
clusterr (#) f ->  negative-yielding ;
coherence
 r (#) f is negative-yielding
proof
let z be real number ; :: according to PARTFUN3:def_2 ::_thesis: ( z in rng (r (#) f) implies 0 > z )
set R = r (#) f;
assume  z in rng (r (#) f) ; ::_thesis: 0 > z
then consider x being set  such that
A1: x in dom (r (#) f) and
A2: (r (#) f) . x = z by FUNCT_1:def_3;
 dom (r (#) f) = 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 real positive number by Def1;
 r * a is negative ;
hence  0 > z by A1, A2, VALUED_1:def_5; ::_thesis: verum
end;
end;

registration
let X be set ;
let r be real positive number ;
let f be positive-yielding PartFunc of X,REAL;
clusterr (#) f ->  positive-yielding ;
coherence
 r (#) f is positive-yielding
proof
let z be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( z in rng (r (#) f) implies 0 < z )
set R = r (#) f;
assume  z in rng (r (#) f) ; ::_thesis: 0 < z
then consider x being set  such that
A1: x in dom (r (#) f) and
A2: (r (#) f) . x = z by FUNCT_1:def_3;
 dom (r (#) f) = 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 real positive number by Def1;
 r * a is positive ;
hence  0 < z by A1, A2, VALUED_1:def_5; ::_thesis: verum
end;
end;

registration
let X be set ;
let r be real negative number ;
let f be negative-yielding PartFunc of X,REAL;
clusterr (#) f ->  positive-yielding ;
coherence
 r (#) f is positive-yielding
proof
let z be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( z in rng (r (#) f) implies 0 < z )
set R = r (#) f;
assume  z in rng (r (#) f) ; ::_thesis: 0 < z
then consider x being set  such that
A1: x in dom (r (#) f) and
A2: (r (#) f) . x = z by FUNCT_1:def_3;
 dom (r (#) f) = 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 real negative number by Def2;
 r * a is positive ;
hence  0 < z by A1, A2, VALUED_1:def_5; ::_thesis: verum
end;
end;

registration
let X be set ;
let r be non zero real number ;
let f be non-empty PartFunc of X,REAL;
clusterr (#) f ->  non-empty ;
coherence
 r (#) f is non-empty
proof
set R = r (#) f;
assume  not r (#) f is non-empty ; ::_thesis: contradiction
then  0 in rng (r (#) f) by RELAT_1:def_9;
then consider x being set  such that
A1: x in dom (r (#) f) and
A2: (r (#) f) . x = 0 by FUNCT_1:def_3;
 dom (r (#) f) = 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 number by RELAT_1:def_9;
 not r * a is zero ;
hence  contradiction by A1, A2, VALUED_1:def_5; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
let f, g be nonpositive-yielding PartFunc of X,REAL;
clusterf / g ->  nonnegative-yielding ;
coherence
 f / g is nonnegative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( r in rng (f / g) implies 0 <= r )
set R = f / g;
assume  r in rng (f / g) ; ::_thesis: 0 <= r
then consider x being set  such that
A1: x in dom (f / g) and
A2: (f / g) . x = r by FUNCT_1:def_3;
A3: dom (f / g) = (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 real non positive number by A4, Def3;
 not a * (b ") is negative ;
hence  0 <= r by A1, A2, RFUNCT_1:def_1; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
let f, g be nonnegative-yielding PartFunc of X,REAL;
clusterf / g ->  nonnegative-yielding ;
coherence
 f / g is nonnegative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( r in rng (f / g) implies 0 <= r )
set R = f / g;
assume  r in rng (f / g) ; ::_thesis: 0 <= r
then consider x being set  such that
A1: x in dom (f / g) and
A2: (f / g) . x = r by FUNCT_1:def_3;
A3: dom (f / g) = (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 real non negative number by A4, Def4;
 not a * (b ") is negative ;
hence  0 <= r by A1, A2, RFUNCT_1:def_1; ::_thesis: verum
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;
clusterf / g ->  nonpositive-yielding ;
coherence
 f / g is nonpositive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_3 ::_thesis: ( r in rng (f / g) implies 0 >= r )
set R = f / g;
assume  r in rng (f / g) ; ::_thesis: 0 >= r
then consider x being set  such that
A1: x in dom (f / g) and
A2: (f / g) . x = r by FUNCT_1:def_3;
A3: dom (f / g) = (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 real non positive number 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 real non negative number by Def4;
 not a * (b ") is positive ;
hence  0 >= r by A1, A2, RFUNCT_1:def_1; ::_thesis: verum
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;
clusterf / g ->  nonpositive-yielding ;
coherence
 f / g is nonpositive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_3 ::_thesis: ( r in rng (f / g) implies 0 >= r )
set R = f / g;
assume  r in rng (f / g) ; ::_thesis: 0 >= r
then consider x being set  such that
A1: x in dom (f / g) and
A2: (f / g) . x = r by FUNCT_1:def_3;
A3: dom (f / g) = (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 real non negative number 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 real non positive number by Def3;
 not a * (b ") is positive ;
hence  0 >= r by A1, A2, RFUNCT_1:def_1; ::_thesis: verum
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;
clusterf / g ->  negative-yielding ;
coherence
 f / g is negative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_2 ::_thesis: ( r in rng (f / g) implies 0 > r )
set R = f / g;
assume  r in rng (f / g) ; ::_thesis: 0 > r
then consider x being set  such that
A1: x in dom (f / g) and
A2: (f / g) . x = r by FUNCT_1:def_3;
A3: dom (f / g) = (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 real positive number 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 real negative number by Def2;
 a * (b ") is negative ;
hence  0 > r by A1, A2, RFUNCT_1:def_1; ::_thesis: verum
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;
clusterf / g ->  negative-yielding ;
coherence
 f / g is negative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_2 ::_thesis: ( r in rng (f / g) implies 0 > r )
set R = f / g;
assume  r in rng (f / g) ; ::_thesis: 0 > r
then consider x being set  such that
A1: x in dom (f / g) and
A2: (f / g) . x = r by FUNCT_1:def_3;
A3: dom (f / g) = (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 real negative number 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 real positive number by Def1;
 a * (b ") is negative ;
hence  0 > r by A1, A2, RFUNCT_1:def_1; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
let f, g be positive-yielding PartFunc of X,REAL;
clusterf / g ->  positive-yielding ;
coherence
 f / g is positive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( r in rng (f / g) implies 0 < r )
set R = f / g;
assume  r in rng (f / g) ; ::_thesis: 0 < r
then consider x being set  such that
A1: x in dom (f / g) and
A2: (f / g) . x = r by FUNCT_1:def_3;
A3: dom (f / g) = (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 real positive number by A4, Def1;
 a * (b ") is positive ;
hence  0 < r by A1, A2, RFUNCT_1:def_1; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
let f, g be negative-yielding PartFunc of X,REAL;
clusterf / g ->  positive-yielding ;
coherence
 f / g is positive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( r in rng (f / g) implies 0 < r )
set R = f / g;
assume  r in rng (f / g) ; ::_thesis: 0 < r
then consider x being set  such that
A1: x in dom (f / g) and
A2: (f / g) . x = r by FUNCT_1:def_3;
A3: dom (f / g) = (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 real negative number by A4, Def2;
 a * (b ") is positive ;
hence  0 < r by A1, A2, RFUNCT_1:def_1; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
let f be PartFunc of X,REAL;
clusterf / f ->  nonnegative-yielding ;
coherence
 f / f is nonnegative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( r in rng (f / f) implies 0 <= r )
set R = f / f;
assume  r in rng (f / f) ; ::_thesis: 0 <= r
then consider x being set  such that
A1: ( x in dom (f / f) & (f / f) . x = r ) by FUNCT_1:def_3;
 not (f . x) * ((f . x) ") is negative ;
hence  0 <= r by A1, RFUNCT_1:def_1; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
let f, g be non-empty PartFunc of X,REAL;
clusterf / g ->  non-empty ;
coherence
 f / g is non-empty
proof
set R = f / g;
assume  not f / g is non-empty ; ::_thesis: contradiction
then  0 in rng (f / g) by RELAT_1:def_9;
then consider x being set  such that
A1: x in dom (f / g) and
A2: (f / g) . x = 0 by FUNCT_1:def_3;
A3: dom (f / g) = (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 number by A4, RELAT_1:def_9;
 not a * (b ") is zero ;
hence  contradiction by A1, A2, RFUNCT_1:def_1; ::_thesis: verum
end;
end;

registration
let X be set ;
let f be nonpositive-yielding Function of X,REAL;
cluster Inv f ->  nonpositive-yielding ;
coherence
 Inv f is nonpositive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_3 ::_thesis: ( r in rng (Inv f) implies 0 >= r )
set R = Inv f;
assume  r in rng (Inv f) ; ::_thesis: 0 >= r
then consider x being set  such that
A1: x in dom (Inv f) and
A2: (Inv f) . x = r by FUNCT_1:def_3;
dom (Inv f) = 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 real non positive number by Def3;
 not a " is positive ;
hence  0 >= r by A2, VALUED_1:10; ::_thesis: verum
end;
end;

registration
let X be set ;
let f be nonnegative-yielding Function of X,REAL;
cluster Inv f ->  nonnegative-yielding ;
coherence
 Inv f is nonnegative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( r in rng (Inv f) implies 0 <= r )
set R = Inv f;
assume  r in rng (Inv f) ; ::_thesis: 0 <= r
then consider x being set  such that
A1: x in dom (Inv f) and
A2: (Inv f) . x = r by FUNCT_1:def_3;
dom (Inv f) = 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 real non negative number by Def4;
 not a " is negative ;
hence  0 <= r by A2, VALUED_1:10; ::_thesis: verum
end;
end;

registration
let X be set ;
let f be positive-yielding Function of X,REAL;
cluster Inv f ->  positive-yielding ;
coherence
 Inv f is positive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( r in rng (Inv f) implies 0 < r )
set R = Inv f;
assume  r in rng (Inv f) ; ::_thesis: 0 < r
then consider x being set  such that
A1: x in dom (Inv f) and
A2: (Inv f) . x = r by FUNCT_1:def_3;
dom (Inv f) = 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 real positive number by Def1;
 a " is positive ;
hence  0 < r by A2, VALUED_1:10; ::_thesis: verum
end;
end;

registration
let X be set ;
let f be negative-yielding Function of X,REAL;
cluster Inv f ->  negative-yielding ;
coherence
 Inv f is negative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_2 ::_thesis: ( r in rng (Inv f) implies 0 > r )
set R = Inv f;
assume  r in rng (Inv f) ; ::_thesis: 0 > r
then consider x being set  such that
A1: x in dom (Inv f) and
A2: (Inv f) . x = r by FUNCT_1:def_3;
dom (Inv f) = 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 real negative number by Def2;
 a " is negative ;
hence  0 > r by A2, VALUED_1:10; ::_thesis: verum
end;
end;

registration
let X be set ;
let f be non-empty Function of X,REAL;
cluster Inv f ->  non-empty ;
coherence
 Inv f is non-empty
proof
set R = Inv f;
assume  not Inv f is non-empty ; ::_thesis: contradiction
then  0 in rng (Inv f) by RELAT_1:def_9;
then consider x being set  such that
A1: x in dom (Inv f) and
A2: (Inv f) . x = 0 by FUNCT_1:def_3;
dom (Inv f) = X by FUNCT_2:def_1
.= dom f by FUNCT_2:def_1 ;
then reconsider a = f . x as non zero real number by A1;
 not a " is zero ;
hence  contradiction by A2, VALUED_1:10; ::_thesis: verum
end;
end;

registration
let X be set ;
let f be non-empty Function of X,REAL;
cluster - f ->  non-empty ;
coherence
 - f is non-empty ;
end;

registration
let X be set ;
let f be nonpositive-yielding Function of X,REAL;
cluster - f ->  nonnegative-yielding ;
coherence
 - f is nonnegative-yielding ;
end;

registration
let X be set ;
let f be nonnegative-yielding Function of X,REAL;
cluster - f ->  nonpositive-yielding ;
coherence
 - f is nonpositive-yielding ;
end;

registration
let X be set ;
let f be positive-yielding Function of X,REAL;
cluster - f ->  negative-yielding ;
coherence
 - f is negative-yielding ;
end;

registration
let X be set ;
let f be negative-yielding Function of X,REAL;
cluster - f ->  positive-yielding ;
coherence
 - f is positive-yielding ;
end;

registration
let X be set ;
let f be Function of X,REAL;
cluster|.f.| ->  nonnegative-yielding ;
coherence
 abs f is nonnegative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( r in rng (abs f) implies 0 <= r )
set R = abs f;
assume  r in rng (abs f) ; ::_thesis: 0 <= r
then consider x being set  such that
 x in dom (abs f) and
A1: (abs f) . x = r by FUNCT_1:def_3;
 not abs (f . x) is negative by COMPLEX1:46;
hence  0 <= r by A1, VALUED_1:18; ::_thesis: verum
end;
end;

registration
let X be set ;
let f be non-empty Function of X,REAL;
cluster|.f.| ->  positive-yielding ;
coherence
 abs f is positive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( r in rng (abs f) implies 0 < r )
set R = abs f;
assume  r in rng (abs f) ; ::_thesis: 0 < r
then consider x being set  such that
A1: x in dom (abs f) and
A2: (abs f) . x = r by FUNCT_1:def_3;
 dom (abs f) = dom f by VALUED_1:def_11;
then reconsider a = f . x as non zero real number by A1;
 abs a is positive by COMPLEX1:47;
hence  0 < r by A2, VALUED_1:18; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
let f be nonpositive-yielding Function of X,REAL;
clusterf ^  ->  nonpositive-yielding ;
coherence
 f ^ is nonpositive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_3 ::_thesis: ( r in rng (f ^) implies 0 >= r )
set R = f ^ ;
assume  r in rng (f ^) ; ::_thesis: 0 >= r
then consider x being set  such that
A1: x in dom (f ^) and
A2: (f ^) . x = r by FUNCT_1:def_3;
 dom (f ^) = (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 real non positive number by Def3;
 not a " is positive ;
hence  0 >= r by A1, A2, RFUNCT_1:def_2; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
let f be nonnegative-yielding Function of X,REAL;
clusterf ^  ->  nonnegative-yielding ;
coherence
 f ^ is nonnegative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( r in rng (f ^) implies 0 <= r )
set R = f ^ ;
assume  r in rng (f ^) ; ::_thesis: 0 <= r
then consider x being set  such that
A1: x in dom (f ^) and
A2: (f ^) . x = r by FUNCT_1:def_3;
 dom (f ^) = (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 real non negative number by Def4;
 not a " is negative ;
hence  0 <= r by A1, A2, RFUNCT_1:def_2; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
let f be positive-yielding Function of X,REAL;
clusterf ^  ->  positive-yielding ;
coherence
 f ^ is positive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( r in rng (f ^) implies 0 < r )
set R = f ^ ;
assume  r in rng (f ^) ; ::_thesis: 0 < r
then consider x being set  such that
A1: x in dom (f ^) and
A2: (f ^) . x = r by FUNCT_1:def_3;
 dom (f ^) = dom f by Th2;
then  f . x in rng f by A1, FUNCT_1:def_3;
then reconsider a = f . x as real positive number by Def1;
 a " is positive ;
hence  0 < r by A1, A2, RFUNCT_1:def_2; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
let f be negative-yielding Function of X,REAL;
clusterf ^  ->  negative-yielding ;
coherence
 f ^ is negative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_2 ::_thesis: ( r in rng (f ^) implies 0 > r )
set R = f ^ ;
assume  r in rng (f ^) ; ::_thesis: 0 > r
then consider x being set  such that
A1: x in dom (f ^) and
A2: (f ^) . x = r by FUNCT_1:def_3;
 dom (f ^) = dom f by Th2;
then  f . x in rng f by A1, FUNCT_1:def_3;
then reconsider a = f . x as real negative number by Def2;
 a " is negative ;
hence  0 > r by A1, A2, RFUNCT_1:def_2; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
let f be non-empty Function of X,REAL;
clusterf ^  ->  non-empty ;
coherence
 f ^ is non-empty
proof
set R = f ^ ;
assume  not f ^ is non-empty ; ::_thesis: contradiction
then  0 in rng (f ^) by RELAT_1:def_9;
then consider x being set  such that
A1: x in dom (f ^) and
A2: (f ^) . x = 0 by FUNCT_1:def_3;
 dom (f ^) = dom f by Th2;
then reconsider a = f . x as non zero real number by A1;
 not a " is zero ;
hence  contradiction by A1, A2, RFUNCT_1:def_2; ::_thesis: verum
end;
end;

definition
let f be real-valued Function;
func sqrt f ->  Function means :Def5: :: PARTFUN3:def 5
( dom it = dom f & ( for x being set st x in dom it holds
it . x = sqrt (f . x) ) );
existence
 ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom b1 holds
b1 . x = sqrt (f . x) ) )
proof
deffunc H1( set ) ->  Element of REAL = sqrt (f . $1);
 ex h being Function st
( dom h = dom f & ( for x being set st x in dom f holds
h . x = H1(x) ) ) from FUNCT_1:sch_3();
hence  ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom b1 holds
b1 . x = sqrt (f . x) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom b1 holds
b1 . x = sqrt (f . x) ) & dom b2 = dom f & ( for x being set st x in dom b2 holds
b2 . x = sqrt (f . x) ) holds
b1 = b2
proof
let h, g be Function; ::_thesis: ( dom h = dom f & ( for x being set st x in dom h holds
h . x = sqrt (f . x) ) & dom g = dom f & ( for x being set st x in dom g holds
g . x = sqrt (f . x) ) implies h = g )
assume that
A1: dom h = dom f and
A2: for c being set st c in dom h holds
h . c = sqrt (f . c) and
A3: dom g = dom f and
A4: for c being set st c in dom g holds
g . c = sqrt (f . c) ; ::_thesis: h = g
now__::_thesis:_for_x_being_set_st_x_in_dom_h_holds_
h_._x_=_g_._x
let x be set ; ::_thesis: ( x in dom h implies h . x = g . x )
assume A5: x in dom h ; ::_thesis: h . x = g . x
hence h . x = sqrt (f . x) by A2
.= g . x by A1, A3, A4, A5 ;
::_thesis: verum
end;
hence  h = g by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines sqrt PARTFUN3:def_5_:_
 for f being real-valued Function
for b2 being Function holds
( b2 = sqrt f iff ( dom b2 = dom f & ( for x being set st x in dom b2 holds
b2 . x = sqrt (f . x) ) ) );

registration
let f be real-valued Function;
cluster sqrt f ->  real-valued ;
coherence
 sqrt f is real-valued
proof
let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (sqrt f) or (sqrt f) . x is real )
set F = sqrt f;
assume  x in dom (sqrt f) ; ::_thesis: (sqrt f) . x is real
then  (sqrt f) . x = sqrt (f . x) by Def5;
hence  (sqrt f) . x is real ; ::_thesis: verum
end;
end;

definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original: sqrt
redefine func sqrt f ->  PartFunc of C,REAL;
coherence
 sqrt f is PartFunc of C,REAL
proof
set F = sqrt f;
 ( dom (sqrt f) = dom f & rng (sqrt f) c= REAL ) by Def5, VALUED_0:def_3;
hence  sqrt f is PartFunc of C,REAL by RELSET_1:4; ::_thesis: verum
end;
end;

registration
let X be set ;
let f be nonnegative-yielding Function of X,REAL;
cluster sqrt f ->  nonnegative-yielding ;
coherence
 sqrt f is nonnegative-yielding
proof
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( r in rng (sqrt f) implies 0 <= r )
set R = sqrt f;
assume  r in rng (sqrt f) ; ::_thesis: 0 <= r
then consider x being set  such that
A1: x in dom (sqrt f) and
A2: (sqrt f) . x = r by FUNCT_1:def_3;
 dom (sqrt f) = dom f by Def5;
then  f . x in rng f by A1, FUNCT_1:def_3;
then reconsider a = f . x as real non negative number by Def4;
 not sqrt a is negative ;
hence  0 <= r by A1, A2, Def5; ::_thesis: verum
end;
end;

registration
let X be set ;
let f be positive-yielding Function of X,REAL;
cluster sqrt f ->  positive-yielding ;
coherence
 sqrt f is positive-yielding
proof
let r be real number ; :: according to PARTFUN3:def_1 ::_thesis: ( r in rng (sqrt f) implies 0 < r )
set R = sqrt f;
assume  r in rng (sqrt f) ; ::_thesis: 0 < r
then consider x being set  such that
A1: x in dom (sqrt f) and
A2: (sqrt f) . x = r by FUNCT_1:def_3;
 dom (sqrt f) = dom f by Def5;
then  f . x in rng f by A1, FUNCT_1:def_3;
then reconsider a = f . x as real positive number by Def1;
 sqrt a is positive ;
hence  0 < r by A1, A2, Def5; ::_thesis: verum
end;
end;

definition
let X be set ;
let f be Function of X,REAL;
:: original: sqrt
redefine func sqrt f ->  Function of X,REAL;
coherence
 sqrt f is Function of X,REAL
proof
dom (sqrt f) = dom f by Def5
.= X by FUNCT_2:def_1 ;
hence  sqrt f is Function of X,REAL by FUNCT_2:def_1; ::_thesis: verum
end;
end;

definition
let X be set ;
let f be non-empty Function of X,REAL;
:: original: ^
redefine funcf ^  ->  Function of X,REAL;
coherence
 f ^ is Function of X,REAL
proof
dom (f ^) = dom f by Th2
.= X by FUNCT_2:def_1 ;
hence  f ^ is Function of X,REAL by FUNCT_2:def_1; ::_thesis: verum
end;
end;

definition
let X be non empty set ;
let f be Function of X,REAL;
let g be non-empty Function of X,REAL;
:: original: /
redefine funcf / g ->  Function of X,REAL;
coherence
 f / g is Function of X,REAL
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  f / g is Function of X,REAL by FUNCT_2:def_1; ::_thesis: verum
end;
end;