:: PARTFUN3 semantic presentation

registration
let c1 be real number ;
cluster a1 / a1 -> non negative ;
coherence
not c1 / c1 is negative
proof end;
end;

registration
let c1 be real number ;
cluster a1 * a1 -> non negative ;
coherence
not c1 * c1 is negative by XREAL_1:65;
cluster a1 * (a1 " ) -> non negative ;
coherence
not c1 * (c1 " ) is negative
proof end;
end;

registration
let c1 be real non negative number ;
cluster sqrt a1 -> non negative ;
coherence
not sqrt c1 is negative by SQUARE_1:def 4;
end;

registration
let c1 be real positive number ;
cluster sqrt a1 -> positive non negative ;
coherence
sqrt c1 is positive by SQUARE_1:93;
end;

theorem Th1: :: PARTFUN3:1
for b1 being Function
for b2 being set st b1 is one-to-one & b2 c= dom (b1 " ) holds
b1 .: ((b1 " ) .: b2) = b2
proof end;

registration
let c1 be non-empty Function;
cluster a1 " {0} -> empty ;
coherence
c1 " {0} is empty
proof end;
end;

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

:: deftheorem Def1 defines positive-yielding PARTFUN3:def 1 :
for b1 being Relation holds
( b1 is positive-yielding iff for b2 being real number st b2 in rng b1 holds
0 < b2 );

:: deftheorem Def2 defines negative-yielding PARTFUN3:def 2 :
for b1 being Relation holds
( b1 is negative-yielding iff for b2 being real number st b2 in rng b1 holds
0 > b2 );

:: deftheorem Def3 defines nonpositive-yielding PARTFUN3:def 3 :
for b1 being Relation holds
( b1 is nonpositive-yielding iff for b2 being real number st b2 in rng b1 holds
0 >= b2 );

:: deftheorem Def4 defines nonnegative-yielding PARTFUN3:def 4 :
for b1 being Relation holds
( b1 is nonnegative-yielding iff for b2 being real number st b2 in rng b1 holds
0 <= b2 );

registration
let c1 be set ;
let c2 be real positive number ;
cluster a1 --> a2 -> positive-yielding ;
coherence
c1 --> c2 is positive-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be real negative number ;
cluster a1 --> a2 -> negative-yielding ;
coherence
c1 --> c2 is negative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be real non positive number ;
cluster a1 --> a2 -> nonpositive-yielding ;
coherence
c1 --> c2 is nonpositive-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be real non negative number ;
cluster a1 --> a2 -> nonnegative-yielding ;
coherence
c1 --> c2 is nonnegative-yielding
proof end;
end;

registration
let c1 be non empty set ;
cluster a1 --> 0 -> non non-empty nonpositive-yielding nonnegative-yielding ;
coherence
not c1 --> 0 is non-empty
proof end;
end;

registration
cluster positive-yielding -> non-empty nonnegative-yielding set ;
coherence
for b1 being Relation st b1 is positive-yielding holds
( b1 is nonnegative-yielding & b1 is non-empty )
proof end;
cluster negative-yielding -> non-empty nonpositive-yielding set ;
coherence
for b1 being Relation st b1 is negative-yielding holds
( b1 is nonpositive-yielding & b1 is non-empty )
proof end;
end;

registration
let c1 be set ;
cluster non-empty negative-yielding nonpositive-yielding Relation of a1, REAL ;
existence
ex b1 being Function of c1, REAL st b1 is negative-yielding
proof end;
cluster non-empty positive-yielding nonnegative-yielding Relation of a1, REAL ;
existence
ex b1 being Function of c1, REAL st b1 is positive-yielding
proof end;
end;

registration
cluster non-empty real-yielding set ;
existence
ex b1 being Function st
( b1 is non-empty & b1 is real-yielding )
proof end;
end;

theorem Th2: :: PARTFUN3:2
for b1 being non-empty real-yielding Function holds dom (b1 ^ ) = dom b1
proof end;

theorem Th3: :: PARTFUN3:3
for b1 being non empty set
for b2 being PartFunc of b1, REAL
for b3 being non-empty PartFunc of b1, REAL holds dom (b2 / b3) = (dom b2) /\ (dom b3)
proof end;

registration
let c1 be set ;
let c2, c3 be nonpositive-yielding PartFunc of c1, REAL ;
cluster a2 + a3 -> nonpositive-yielding ;
coherence
c2 + c3 is nonpositive-yielding
proof end;
end;

registration
let c1 be set ;
let c2, c3 be nonnegative-yielding PartFunc of c1, REAL ;
cluster a2 + a3 -> nonnegative-yielding ;
coherence
c2 + c3 is nonnegative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be positive-yielding PartFunc of c1, REAL ;
let c3 be nonnegative-yielding PartFunc of c1, REAL ;
cluster a2 + a3 -> non-empty positive-yielding nonnegative-yielding ;
coherence
c2 + c3 is positive-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be nonnegative-yielding PartFunc of c1, REAL ;
let c3 be positive-yielding PartFunc of c1, REAL ;
cluster a2 + a3 -> non-empty positive-yielding nonnegative-yielding ;
coherence
c2 + c3 is positive-yielding ;
end;

registration
let c1 be set ;
let c2 be nonpositive-yielding PartFunc of c1, REAL ;
let c3 be negative-yielding PartFunc of c1, REAL ;
cluster a2 + a3 -> non-empty negative-yielding nonpositive-yielding ;
coherence
c2 + c3 is negative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be negative-yielding PartFunc of c1, REAL ;
let c3 be nonpositive-yielding PartFunc of c1, REAL ;
cluster a2 + a3 -> non-empty negative-yielding nonpositive-yielding ;
coherence
c2 + c3 is negative-yielding ;
end;

registration
let c1 be set ;
let c2 be nonnegative-yielding PartFunc of c1, REAL ;
let c3 be nonpositive-yielding PartFunc of c1, REAL ;
cluster a2 - a3 -> nonnegative-yielding ;
coherence
c2 - c3 is nonnegative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be nonpositive-yielding PartFunc of c1, REAL ;
let c3 be nonnegative-yielding PartFunc of c1, REAL ;
cluster a2 - a3 -> nonpositive-yielding ;
coherence
c2 - c3 is nonpositive-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be positive-yielding PartFunc of c1, REAL ;
let c3 be nonpositive-yielding PartFunc of c1, REAL ;
cluster a2 - a3 -> non-empty positive-yielding nonnegative-yielding ;
coherence
c2 - c3 is positive-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be nonpositive-yielding PartFunc of c1, REAL ;
let c3 be positive-yielding PartFunc of c1, REAL ;
cluster a2 - a3 -> non-empty negative-yielding nonpositive-yielding ;
coherence
c2 - c3 is negative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be negative-yielding PartFunc of c1, REAL ;
let c3 be nonnegative-yielding PartFunc of c1, REAL ;
cluster a2 - a3 -> non-empty negative-yielding nonpositive-yielding ;
coherence
c2 - c3 is negative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be nonnegative-yielding PartFunc of c1, REAL ;
let c3 be negative-yielding PartFunc of c1, REAL ;
cluster a2 - a3 -> non-empty positive-yielding nonnegative-yielding ;
coherence
c2 - c3 is positive-yielding
proof end;
end;

registration
let c1 be set ;
let c2, c3 be nonpositive-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> nonnegative-yielding ;
coherence
c2 (#) c3 is nonnegative-yielding
proof end;
end;

registration
let c1 be set ;
let c2, c3 be nonnegative-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> nonnegative-yielding ;
coherence
c2 (#) c3 is nonnegative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be nonpositive-yielding PartFunc of c1, REAL ;
let c3 be nonnegative-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> nonpositive-yielding ;
coherence
c2 (#) c3 is nonpositive-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be nonnegative-yielding PartFunc of c1, REAL ;
let c3 be nonpositive-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> nonpositive-yielding ;
coherence
c2 (#) c3 is nonpositive-yielding ;
end;

registration
let c1 be set ;
let c2 be positive-yielding PartFunc of c1, REAL ;
let c3 be negative-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> non-empty negative-yielding nonpositive-yielding ;
coherence
c2 (#) c3 is negative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be negative-yielding PartFunc of c1, REAL ;
let c3 be positive-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> non-empty negative-yielding nonpositive-yielding ;
coherence
c2 (#) c3 is negative-yielding ;
end;

registration
let c1 be set ;
let c2, c3 be positive-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> non-empty positive-yielding nonnegative-yielding ;
coherence
c2 (#) c3 is positive-yielding
proof end;
end;

registration
let c1 be set ;
let c2, c3 be negative-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> non-empty positive-yielding nonnegative-yielding ;
coherence
c2 (#) c3 is positive-yielding
proof end;
end;

registration
let c1 be set ;
let c2, c3 be non-empty PartFunc of c1, REAL ;
cluster a2 (#) a3 -> non-empty ;
coherence
c2 (#) c3 is non-empty
proof end;
end;

registration
let c1 be set ;
let c2 be PartFunc of c1, REAL ;
cluster a2 (#) a2 -> nonnegative-yielding ;
coherence
c2 (#) c2 is nonnegative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be real non positive number ;
let c3 be nonpositive-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> nonnegative-yielding ;
coherence
c2 (#) c3 is nonnegative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be real non negative number ;
let c3 be nonnegative-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> nonnegative-yielding ;
coherence
c2 (#) c3 is nonnegative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be real non positive number ;
let c3 be nonnegative-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> nonpositive-yielding ;
coherence
c2 (#) c3 is nonpositive-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be real non negative number ;
let c3 be nonpositive-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> nonpositive-yielding ;
coherence
c2 (#) c3 is nonpositive-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be real positive number ;
let c3 be negative-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> non-empty negative-yielding nonpositive-yielding ;
coherence
c2 (#) c3 is negative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be real negative number ;
let c3 be positive-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> non-empty negative-yielding nonpositive-yielding ;
coherence
c2 (#) c3 is negative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be real positive number ;
let c3 be positive-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> non-empty positive-yielding nonnegative-yielding ;
coherence
c2 (#) c3 is positive-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be real negative number ;
let c3 be negative-yielding PartFunc of c1, REAL ;
cluster a2 (#) a3 -> non-empty positive-yielding nonnegative-yielding ;
coherence
c2 (#) c3 is positive-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be non zero real number ;
let c3 be non-empty PartFunc of c1, REAL ;
cluster a2 (#) a3 -> non-empty ;
coherence
c2 (#) c3 is non-empty
proof end;
end;

registration
let c1 be non empty set ;
let c2, c3 be nonpositive-yielding PartFunc of c1, REAL ;
cluster a2 / a3 -> nonnegative-yielding ;
coherence
c2 / c3 is nonnegative-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2, c3 be nonnegative-yielding PartFunc of c1, REAL ;
cluster a2 / a3 -> nonnegative-yielding ;
coherence
c2 / c3 is nonnegative-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2 be nonpositive-yielding PartFunc of c1, REAL ;
let c3 be nonnegative-yielding PartFunc of c1, REAL ;
cluster a2 / a3 -> nonpositive-yielding ;
coherence
c2 / c3 is nonpositive-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2 be nonnegative-yielding PartFunc of c1, REAL ;
let c3 be nonpositive-yielding PartFunc of c1, REAL ;
cluster a2 / a3 -> nonpositive-yielding ;
coherence
c2 / c3 is nonpositive-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2 be positive-yielding PartFunc of c1, REAL ;
let c3 be negative-yielding PartFunc of c1, REAL ;
cluster a2 / a3 -> non-empty negative-yielding nonpositive-yielding ;
coherence
c2 / c3 is negative-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2 be negative-yielding PartFunc of c1, REAL ;
let c3 be positive-yielding PartFunc of c1, REAL ;
cluster a2 / a3 -> non-empty negative-yielding nonpositive-yielding ;
coherence
c2 / c3 is negative-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2, c3 be positive-yielding PartFunc of c1, REAL ;
cluster a2 / a3 -> non-empty positive-yielding nonnegative-yielding ;
coherence
c2 / c3 is positive-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2, c3 be negative-yielding PartFunc of c1, REAL ;
cluster a2 / a3 -> non-empty positive-yielding nonnegative-yielding ;
coherence
c2 / c3 is positive-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2 be PartFunc of c1, REAL ;
cluster a2 / a2 -> nonnegative-yielding ;
coherence
c2 / c2 is nonnegative-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2, c3 be non-empty PartFunc of c1, REAL ;
cluster a2 / a3 -> non-empty ;
coherence
c2 / c3 is non-empty
proof end;
end;

registration
let c1 be set ;
let c2 be nonpositive-yielding Function of c1, REAL ;
cluster Inv a2 -> nonpositive-yielding ;
coherence
Inv c2 is nonpositive-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be nonnegative-yielding Function of c1, REAL ;
cluster Inv a2 -> nonnegative-yielding ;
coherence
Inv c2 is nonnegative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be positive-yielding Function of c1, REAL ;
cluster Inv a2 -> non-empty positive-yielding nonnegative-yielding ;
coherence
Inv c2 is positive-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be negative-yielding Function of c1, REAL ;
cluster Inv a2 -> non-empty negative-yielding nonpositive-yielding ;
coherence
Inv c2 is negative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be non-empty Function of c1, REAL ;
cluster Inv a2 -> non-empty ;
coherence
Inv c2 is non-empty
proof end;
end;

registration
let c1 be set ;
let c2 be non-empty Function of c1, REAL ;
cluster - a2 -> non-empty ;
coherence
- c2 is non-empty
proof end;
end;

registration
let c1 be set ;
let c2 be nonpositive-yielding Function of c1, REAL ;
cluster - a2 -> nonnegative-yielding ;
coherence
- c2 is nonnegative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be nonnegative-yielding Function of c1, REAL ;
cluster - a2 -> nonpositive-yielding ;
coherence
- c2 is nonpositive-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be positive-yielding Function of c1, REAL ;
cluster - a2 -> non-empty negative-yielding nonpositive-yielding ;
coherence
- c2 is negative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be negative-yielding Function of c1, REAL ;
cluster - a2 -> non-empty positive-yielding nonnegative-yielding ;
coherence
- c2 is positive-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be Function of c1, REAL ;
cluster abs a2 -> nonnegative-yielding ;
coherence
abs c2 is nonnegative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be non-empty Function of c1, REAL ;
cluster abs a2 -> non-empty positive-yielding nonnegative-yielding ;
coherence
abs c2 is positive-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2 be nonpositive-yielding Function of c1, REAL ;
cluster a2 ^ -> nonpositive-yielding ;
coherence
c2 ^ is nonpositive-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2 be nonnegative-yielding Function of c1, REAL ;
cluster a2 ^ -> nonnegative-yielding ;
coherence
c2 ^ is nonnegative-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2 be positive-yielding Function of c1, REAL ;
cluster a2 ^ -> non-empty positive-yielding nonnegative-yielding ;
coherence
c2 ^ is positive-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2 be negative-yielding Function of c1, REAL ;
cluster a2 ^ -> non-empty negative-yielding nonpositive-yielding ;
coherence
c2 ^ is negative-yielding
proof end;
end;

registration
let c1 be non empty set ;
let c2 be non-empty Function of c1, REAL ;
cluster a2 ^ -> non-empty ;
coherence
c2 ^ is non-empty
proof end;
end;

definition
let c1 be real-yielding Function;
func sqrt c1 -> Function means :Def5: :: PARTFUN3:def 5
( dom a2 = dom a1 & ( for b1 being set st b1 in dom a2 holds
a2 . b1 = sqrt (a1 . b1) ) );
existence
ex b1 being Function st
( dom b1 = dom c1 & ( for b2 being set st b2 in dom b1 holds
b1 . b2 = sqrt (c1 . b2) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom c1 & ( for b3 being set st b3 in dom b1 holds
b1 . b3 = sqrt (c1 . b3) ) & dom b2 = dom c1 & ( for b3 being set st b3 in dom b2 holds
b2 . b3 = sqrt (c1 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines sqrt PARTFUN3:def 5 :
for b1 being real-yielding Function
for b2 being Function holds
( b2 = sqrt b1 iff ( dom b2 = dom b1 & ( for b3 being set st b3 in dom b2 holds
b2 . b3 = sqrt (b1 . b3) ) ) );

registration
let c1 be real-yielding Function;
cluster sqrt a1 -> real-yielding ;
coherence
sqrt c1 is real-yielding
proof end;
end;

definition
let c1 be set ;
let c2 be real-membered set ;
let c3 be PartFunc of c1,c2;
redefine func sqrt as sqrt c3 -> PartFunc of a1, REAL ;
coherence
sqrt c3 is PartFunc of c1, REAL
proof end;
end;

registration
let c1 be set ;
let c2 be nonnegative-yielding Function of c1, REAL ;
cluster sqrt a2 -> real-yielding nonnegative-yielding ;
coherence
sqrt c2 is nonnegative-yielding
proof end;
end;

registration
let c1 be set ;
let c2 be positive-yielding Function of c1, REAL ;
cluster sqrt a2 -> non-empty real-yielding positive-yielding nonnegative-yielding ;
coherence
sqrt c2 is positive-yielding
proof end;
end;

definition
let c1 be set ;
let c2, c3 be Function of c1, REAL ;
redefine func + as c2 + c3 -> Function of a1, REAL ;
coherence
c2 + c3 is Function of c1, REAL
proof end;
redefine func - as c2 - c3 -> Function of a1, REAL ;
coherence
c2 - c3 is Function of c1, REAL
proof end;
redefine func (#) as c2 (#) c3 -> Function of a1, REAL ;
coherence
c2 (#) c3 is Function of c1, REAL
proof end;
end;

definition
let c1 be set ;
let c2 be Function of c1, REAL ;
redefine func - as - c2 -> Function of a1, REAL ;
coherence
- c2 is Function of c1, REAL
proof end;
redefine func abs as abs c2 -> Function of a1, REAL ;
coherence
abs c2 is Function of c1, REAL
proof end;
redefine func sqrt as sqrt c2 -> Function of a1, REAL ;
coherence
sqrt c2 is Function of c1, REAL
proof end;
end;

definition
let c1 be set ;
let c2 be Function of c1, REAL ;
let c3 be real number ;
redefine func (#) as c3 (#) c2 -> Function of a1, REAL ;
coherence
c3 (#) c2 is Function of c1, REAL
proof end;
end;

definition
let c1 be set ;
let c2 be non-empty Function of c1, REAL ;
redefine func ^ as c2 ^ -> Function of a1, REAL ;
coherence
c2 ^ is Function of c1, REAL
proof end;
end;

definition
let c1 be non empty set ;
let c2 be Function of c1, REAL ;
let c3 be non-empty Function of c1, REAL ;
redefine func / as c2 / c3 -> Function of a1, REAL ;
coherence
c2 / c3 is Function of c1, REAL
proof end;
end;

definition
let c1 be non empty TopSpace;
let c2, c3 be continuous RealMap of c1;
set c4 = the carrier of c1;
redefine func + as c2 + c3 -> continuous RealMap of a1;
coherence
c2 + c3 is continuous RealMap of c1
proof end;
redefine func - as c2 - c3 -> continuous RealMap of a1;
coherence
c2 - c3 is continuous RealMap of c1
proof end;
redefine func (#) as c2 (#) c3 -> continuous RealMap of a1;
coherence
c2 (#) c3 is continuous RealMap of c1
proof end;
end;

definition
let c1 be non empty TopSpace;
let c2 be continuous RealMap of c1;
redefine func - as - c2 -> continuous RealMap of a1;
coherence
- c2 is continuous RealMap of c1
proof end;
end;

definition
let c1 be non empty TopSpace;
let c2 be continuous RealMap of c1;
redefine func abs as abs c2 -> continuous RealMap of a1;
coherence
abs c2 is continuous RealMap of c1
proof end;
end;

E8: now
let c1 be non empty TopSpace;
let c2 be Real;
set c3 = the carrier of c1;
set c4 = the carrier of c1 --> c2;
thus the carrier of c1 --> c2 is continuous
proof
E9: dom (the carrier of c1 --> c2) = the carrier of c1 by FUNCT_2:def 1;
E10: rng (the carrier of c1 --> c2) = {c2} by FUNCOP_1:14;
let c5 be Subset of REAL ; :: according to PSCOMP_1:def 25
assume c5 is closed ;
per cases ( c2 in c5 or not c2 in c5 ) ;
suppose c2 in c5 ;
then E11: rng (the carrier of c1 --> c2) c= c5 by E10, ZFMISC_1:37;
(the carrier of c1 --> c2) " c5 = (the carrier of c1 --> c2) " ((rng (the carrier of c1 --> c2)) /\ c5) by RELAT_1:168
.= (the carrier of c1 --> c2) " (rng (the carrier of c1 --> c2)) by E11, XBOOLE_1:28
.= the carrier of c1 by E9, RELAT_1:169
.= [#] c1 by PRE_TOPC:12 ;
hence (the carrier of c1 --> c2) " c5 is closed ;
end;
suppose not c2 in c5 ;
then E11: rng (the carrier of c1 --> c2) misses c5 by E10, ZFMISC_1:56;
(the carrier of c1 --> c2) " c5 = (the carrier of c1 --> c2) " ((rng (the carrier of c1 --> c2)) /\ c5) by RELAT_1:168
.= (the carrier of c1 --> c2) " {} by E11, XBOOLE_0:def 7
.= {} c1 by RELAT_1:171 ;
hence (the carrier of c1 --> c2) " c5 is closed ;
end;
end;
end;
end;

registration
let c1 be non empty TopSpace;
cluster non-empty continuous positive-yielding nonnegative-yielding Relation of the carrier of a1, REAL ;
existence
ex b1 being RealMap of c1 st
( b1 is positive-yielding & b1 is continuous )
proof end;
cluster non-empty continuous negative-yielding nonpositive-yielding Relation of the carrier of a1, REAL ;
existence
ex b1 being RealMap of c1 st
( b1 is negative-yielding & b1 is continuous )
proof end;
end;

definition
let c1 be non empty TopSpace;
let c2 be continuous nonnegative-yielding RealMap of c1;
redefine func sqrt as sqrt c2 -> continuous RealMap of a1;
coherence
sqrt c2 is continuous RealMap of c1
proof end;
end;

definition
let c1 be non empty TopSpace;
let c2 be continuous RealMap of c1;
let c3 be real number ;
redefine func (#) as c3 (#) c2 -> continuous RealMap of a1;
coherence
c3 (#) c2 is continuous RealMap of c1
proof end;
end;

definition
let c1 be non empty TopSpace;
let c2 be non-empty continuous RealMap of c1;
redefine func ^ as c2 ^ -> continuous RealMap of a1;
coherence
c2 ^ is continuous RealMap of c1
proof end;
end;

definition
let c1 be non empty TopSpace;
let c2 be continuous RealMap of c1;
let c3 be non-empty continuous RealMap of c1;
redefine func / as c2 / c3 -> continuous RealMap of a1;
coherence
c2 / c3 is continuous RealMap of c1
proof end;
end;