:: PARTFUN3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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

registration
let r be real number ;
cluster r * r -> non negative ;
coherence
not r * r is negative by XREAL_1:65;
cluster r * (r " ) -> non negative ;
coherence
not r * (r " ) is negative
proof 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 4;
end;

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

theorem :: PARTFUN3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function
for A being set st f is one-to-one & A c= dom (f " ) holds
f .: ((f " ) .: A) = A
proof end;

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

definition
let R be Relation;
attr R is positive-yielding means :Def1: :: PARTFUN3:def 1
for r being real number st r in rng R holds
0 < r;
attr R is negative-yielding means :Def2: :: PARTFUN3:def 2
for r being real number st r in rng R holds
0 > r;
attr R is nonpositive-yielding means :Def3: :: PARTFUN3:def 3
for r being real number st r in rng R holds
0 >= r;
attr R 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 ;
cluster X --> r -> positive-yielding ;
coherence
X --> r is positive-yielding
proof end;
end;

registration
let X be set ;
let r be real negative number ;
cluster X --> r -> negative-yielding ;
coherence
X --> r is negative-yielding
proof end;
end;

registration
let X be set ;
let r be real non positive number ;
cluster X --> r -> nonpositive-yielding ;
coherence
X --> r is nonpositive-yielding
proof end;
end;

registration
let X be set ;
let r be real non negative number ;
cluster X --> r -> nonnegative-yielding ;
coherence
X --> r is nonnegative-yielding
proof end;
end;

registration
let X be non empty set ;
cluster X --> 0 -> non non-empty nonpositive-yielding nonnegative-yielding ;
coherence
not X --> 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 X be set ;
cluster non-empty negative-yielding nonpositive-yielding Relation of X, REAL ;
existence
ex b1 being Function of X, REAL st b1 is negative-yielding
proof end;
cluster non-empty positive-yielding nonnegative-yielding Relation of X, REAL ;
existence
ex b1 being Function of X, 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non-empty real-yielding Function holds dom (f ^ ) = dom f
proof end;

theorem Th3: :: PARTFUN3:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 end;

registration
let X be set ;
let f, g be nonpositive-yielding PartFunc of X, REAL ;
cluster f + g -> nonpositive-yielding ;
coherence
f + g is nonpositive-yielding
proof end;
end;

registration
let X be set ;
let f, g be nonnegative-yielding PartFunc of X, REAL ;
cluster f + g -> nonnegative-yielding ;
coherence
f + g is nonnegative-yielding
proof end;
end;

registration
let X be set ;
let f be positive-yielding PartFunc of X, REAL ;
let g be nonnegative-yielding PartFunc of X, REAL ;
cluster f + g -> non-empty positive-yielding nonnegative-yielding ;
coherence
f + g is positive-yielding
proof end;
end;

registration
let X be set ;
let f be nonnegative-yielding PartFunc of X, REAL ;
let g be positive-yielding PartFunc of X, REAL ;
cluster f + g -> non-empty positive-yielding nonnegative-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 ;
cluster f + g -> non-empty negative-yielding nonpositive-yielding ;
coherence
f + g is negative-yielding
proof end;
end;

registration
let X be set ;
let f be negative-yielding PartFunc of X, REAL ;
let g be nonpositive-yielding PartFunc of X, REAL ;
cluster f + g -> non-empty negative-yielding nonpositive-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 ;
cluster f - g -> nonnegative-yielding ;
coherence
f - g is nonnegative-yielding
proof end;
end;

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

registration
let X be set ;
let f be positive-yielding PartFunc of X, REAL ;
let g be nonpositive-yielding PartFunc of X, REAL ;
cluster f - g -> non-empty positive-yielding nonnegative-yielding ;
coherence
f - g is positive-yielding
proof end;
end;

registration
let X be set ;
let f be nonpositive-yielding PartFunc of X, REAL ;
let g be positive-yielding PartFunc of X, REAL ;
cluster f - g -> non-empty negative-yielding nonpositive-yielding ;
coherence
f - g is negative-yielding
proof end;
end;

registration
let X be set ;
let f be negative-yielding PartFunc of X, REAL ;
let g be nonnegative-yielding PartFunc of X, REAL ;
cluster f - g -> non-empty negative-yielding nonpositive-yielding ;
coherence
f - g is negative-yielding
proof end;
end;

registration
let X be set ;
let f be nonnegative-yielding PartFunc of X, REAL ;
let g be negative-yielding PartFunc of X, REAL ;
cluster f - g -> non-empty positive-yielding nonnegative-yielding ;
coherence
f - g is positive-yielding
proof end;
end;

registration
let X be set ;
let f, g be nonpositive-yielding PartFunc of X, REAL ;
cluster f (#) g -> nonnegative-yielding ;
coherence
f (#) g is nonnegative-yielding
proof end;
end;

registration
let X be set ;
let f, g be nonnegative-yielding PartFunc of X, REAL ;
cluster f (#) g -> nonnegative-yielding ;
coherence
f (#) g is nonnegative-yielding
proof end;
end;

registration
let X be set ;
let f be nonpositive-yielding PartFunc of X, REAL ;
let g be nonnegative-yielding PartFunc of X, REAL ;
cluster f (#) g -> nonpositive-yielding ;
coherence
f (#) g is nonpositive-yielding
proof end;
end;

registration
let X be set ;
let f be nonnegative-yielding PartFunc of X, REAL ;
let g be nonpositive-yielding PartFunc of X, REAL ;
cluster f (#) g -> nonpositive-yielding ;
coherence
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 ;
cluster f (#) g -> non-empty negative-yielding nonpositive-yielding ;
coherence
f (#) g is negative-yielding
proof end;
end;

registration
let X be set ;
let f be negative-yielding PartFunc of X, REAL ;
let g be positive-yielding PartFunc of X, REAL ;
cluster f (#) g -> non-empty negative-yielding nonpositive-yielding ;
coherence
f (#) g is negative-yielding ;
end;

registration
let X be set ;
let f, g be positive-yielding PartFunc of X, REAL ;
cluster f (#) g -> non-empty positive-yielding nonnegative-yielding ;
coherence
f (#) g is positive-yielding
proof end;
end;

registration
let X be set ;
let f, g be negative-yielding PartFunc of X, REAL ;
cluster f (#) g -> non-empty positive-yielding nonnegative-yielding ;
coherence
f (#) g is positive-yielding
proof end;
end;

registration
let X be set ;
let f, g be non-empty PartFunc of X, REAL ;
cluster f (#) g -> non-empty ;
coherence
f (#) g is non-empty
proof end;
end;

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

registration
let X be set ;
let r be real non positive number ;
let f be nonpositive-yielding PartFunc of X, REAL ;
cluster r (#) f -> nonnegative-yielding ;
coherence
r (#) f is nonnegative-yielding
proof end;
end;

registration
let X be set ;
let r be real non negative number ;
let f be nonnegative-yielding PartFunc of X, REAL ;
cluster r (#) f -> nonnegative-yielding ;
coherence
r (#) f is nonnegative-yielding
proof end;
end;

registration
let X be set ;
let r be real non positive number ;
let f be nonnegative-yielding PartFunc of X, REAL ;
cluster r (#) f -> nonpositive-yielding ;
coherence
r (#) f is nonpositive-yielding
proof end;
end;

registration
let X be set ;
let r be real non negative number ;
let f be nonpositive-yielding PartFunc of X, REAL ;
cluster r (#) f -> nonpositive-yielding ;
coherence
r (#) f is nonpositive-yielding
proof end;
end;

registration
let X be set ;
let r be real positive number ;
let f be negative-yielding PartFunc of X, REAL ;
cluster r (#) f -> non-empty negative-yielding nonpositive-yielding ;
coherence
r (#) f is negative-yielding
proof end;
end;

registration
let X be set ;
let r be real negative number ;
let f be positive-yielding PartFunc of X, REAL ;
cluster r (#) f -> non-empty negative-yielding nonpositive-yielding ;
coherence
r (#) f is negative-yielding
proof end;
end;

registration
let X be set ;
let r be real positive number ;
let f be positive-yielding PartFunc of X, REAL ;
cluster r (#) f -> non-empty positive-yielding nonnegative-yielding ;
coherence
r (#) f is positive-yielding
proof end;
end;

registration
let X be set ;
let r be real negative number ;
let f be negative-yielding PartFunc of X, REAL ;
cluster r (#) f -> non-empty positive-yielding nonnegative-yielding ;
coherence
r (#) f is positive-yielding
proof end;
end;

registration
let X be set ;
let r be non zero real number ;
let f be non-empty PartFunc of X, REAL ;
cluster r (#) f -> non-empty ;
coherence
r (#) f is non-empty
proof end;
end;

registration
let X be non empty set ;
let f, g be nonpositive-yielding PartFunc of X, REAL ;
cluster f / g -> nonnegative-yielding ;
coherence
f / g is nonnegative-yielding
proof end;
end;

registration
let X be non empty set ;
let f, g be nonnegative-yielding PartFunc of X, REAL ;
cluster f / g -> nonnegative-yielding ;
coherence
f / g is nonnegative-yielding
proof end;
end;

registration
let X be non empty set ;
let f be nonpositive-yielding PartFunc of X, REAL ;
let g be nonnegative-yielding PartFunc of X, REAL ;
cluster f / g -> nonpositive-yielding ;
coherence
f / g is nonpositive-yielding
proof end;
end;

registration
let X be non empty set ;
let f be nonnegative-yielding PartFunc of X, REAL ;
let g be nonpositive-yielding PartFunc of X, REAL ;
cluster f / g -> nonpositive-yielding ;
coherence
f / g is nonpositive-yielding
proof end;
end;

registration
let X be non empty set ;
let f be positive-yielding PartFunc of X, REAL ;
let g be negative-yielding PartFunc of X, REAL ;
cluster f / g -> non-empty negative-yielding nonpositive-yielding ;
coherence
f / g is negative-yielding
proof end;
end;

registration
let X be non empty set ;
let f be negative-yielding PartFunc of X, REAL ;
let g be positive-yielding PartFunc of X, REAL ;
cluster f / g -> non-empty negative-yielding nonpositive-yielding ;
coherence
f / g is negative-yielding
proof end;
end;

registration
let X be non empty set ;
let f, g be positive-yielding PartFunc of X, REAL ;
cluster f / g -> non-empty positive-yielding nonnegative-yielding ;
coherence
f / g is positive-yielding
proof end;
end;

registration
let X be non empty set ;
let f, g be negative-yielding PartFunc of X, REAL ;
cluster f / g -> non-empty positive-yielding nonnegative-yielding ;
coherence
f / g is positive-yielding
proof end;
end;

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

registration
let X be non empty set ;
let f, g be non-empty PartFunc of X, REAL ;
cluster f / g -> non-empty ;
coherence
f / g is non-empty
proof 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 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 end;
end;

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

registration
let X be set ;
let f be negative-yielding Function of X, REAL ;
cluster Inv f -> non-empty negative-yielding nonpositive-yielding ;
coherence
Inv f is negative-yielding
proof 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 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
proof end;
end;

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

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

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

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

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

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

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

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

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

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

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

definition
let f be real-yielding 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 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 end;
end;

:: deftheorem Def5 defines sqrt PARTFUN3:def 5 :
for f being real-yielding 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-yielding Function;
cluster sqrt f -> real-yielding ;
coherence
sqrt f is real-yielding
proof 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 end;
end;

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

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

definition
let X be set ;
let f, g be Function of X, REAL ;
:: original: +
redefine func f + g -> Function of X, REAL ;
coherence
f + g is Function of X, REAL
proof end;
:: original: -
redefine func f - g -> Function of X, REAL ;
coherence
f - g is Function of X, REAL
proof end;
:: original: (#)
redefine func f (#) g -> Function of X, REAL ;
coherence
f (#) g is Function of X, REAL
proof end;
end;

definition
let X be set ;
let f be Function of X, REAL ;
:: original: -
redefine func - f -> Function of X, REAL ;
coherence
- f is Function of X, REAL
proof end;
:: original: abs
redefine func abs f -> Function of X, REAL ;
coherence
abs f is Function of X, REAL
proof end;
:: original: sqrt
redefine func sqrt f -> Function of X, REAL ;
coherence
sqrt f is Function of X, REAL
proof end;
end;

definition
let X be set ;
let f be Function of X, REAL ;
let r be real number ;
:: original: (#)
redefine func r (#) f -> Function of X, REAL ;
coherence
r (#) f is Function of X, REAL
proof end;
end;

definition
let X be set ;
let f be non-empty Function of X, REAL ;
:: original: ^
redefine func f ^ -> Function of X, REAL ;
coherence
f ^ is Function of X, REAL
proof 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 func f / g -> Function of X, REAL ;
coherence
f / g is Function of X, REAL
proof end;
end;

definition
let T be non empty TopSpace;
let f, g be continuous RealMap of T;
set c = the carrier of T;
:: original: +
redefine func f + g -> continuous RealMap of T;
coherence
f + g is continuous RealMap of T
proof end;
:: original: -
redefine func f - g -> continuous RealMap of T;
coherence
f - g is continuous RealMap of T
proof end;
:: original: (#)
redefine func f (#) g -> continuous RealMap of T;
coherence
f (#) g is continuous RealMap of T
proof end;
end;

definition
let T be non empty TopSpace;
let f be continuous RealMap of T;
:: original: -
redefine func - f -> continuous RealMap of T;
coherence
- f is continuous RealMap of T
proof end;
end;

definition
let T be non empty TopSpace;
let f be continuous RealMap of T;
:: original: abs
redefine func abs f -> continuous RealMap of T;
coherence
abs f is continuous RealMap of T
proof end;
end;

Lm1: now
let T be non empty TopSpace; :: thesis: for a being Real holds the carrier of T --> a is continuous
let a be Real; :: thesis: the carrier of T --> a is continuous
set c = the carrier of T;
set f = the carrier of T --> a;
thus the carrier of T --> a is continuous :: thesis: verum
proof
A1: dom (the carrier of T --> a) = the carrier of T by FUNCT_2:def 1;
A2: rng (the carrier of T --> a) = {a} by FUNCOP_1:14;
let Y be Subset of REAL ; :: according to PSCOMP_1:def 25 :: thesis: ( not Y is closed or (the carrier of T --> a) " Y is closed )
assume Y is closed ; :: thesis: (the carrier of T --> a) " Y is closed
per cases ( a in Y or not a in Y ) ;
suppose a in Y ; :: thesis: (the carrier of T --> a) " Y is closed
then A3: rng (the carrier of T --> a) c= Y by A2, ZFMISC_1:37;
(the carrier of T --> a) " Y = (the carrier of T --> a) " ((rng (the carrier of T --> a)) /\ Y) by RELAT_1:168
.= (the carrier of T --> a) " (rng (the carrier of T --> a)) by A3, XBOOLE_1:28
.= the carrier of T by A1, RELAT_1:169
.= [#] T by PRE_TOPC:12 ;
hence (the carrier of T --> a) " Y is closed ; :: thesis: verum
end;
suppose not a in Y ; :: thesis: (the carrier of T --> a) " Y is closed
then A4: rng (the carrier of T --> a) misses Y by A2, ZFMISC_1:56;
(the carrier of T --> a) " Y = (the carrier of T --> a) " ((rng (the carrier of T --> a)) /\ Y) by RELAT_1:168
.= (the carrier of T --> a) " {} by A4, XBOOLE_0:def 7
.= {} T by RELAT_1:171 ;
hence (the carrier of T --> a) " Y is closed ; :: thesis: verum
end;
end;
end;
end;

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

definition
let T be non empty TopSpace;
let f be continuous nonnegative-yielding RealMap of T;
:: original: sqrt
redefine func sqrt f -> continuous RealMap of T;
coherence
sqrt f is continuous RealMap of T
proof end;
end;

definition
let T be non empty TopSpace;
let f be continuous RealMap of T;
let r be real number ;
:: original: (#)
redefine func r (#) f -> continuous RealMap of T;
coherence
r (#) f is continuous RealMap of T
proof end;
end;

definition
let T be non empty TopSpace;
let f be non-empty continuous RealMap of T;
:: original: ^
redefine func f ^ -> continuous RealMap of T;
coherence
f ^ is continuous RealMap of T
proof end;
end;

definition
let T be non empty TopSpace;
let f be continuous RealMap of T;
let g be non-empty continuous RealMap of T;
:: original: /
redefine func f / g -> continuous RealMap of T;
coherence
f / g is continuous RealMap of T
proof end;
end;