:: PARTFUN4 semantic presentation

begin


registration
let T be non empty TopSpace;
let f, g be continuous RealMap of T;
set c = the carrier of T;
reconsider F = f, G = g as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17;
clusterf + g ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = f + g holds
b1 is continuous
proof
consider H being Function of T,R^1 such that
A1: for p being Point of T
for r1, r2 being real number st F . p = r1 & G . p = r2 holds
H . p = r1 + r2 and
A2: H is continuous by JGRAPH_2:19;
reconsider h = H as RealMap of T by TOPMETR:17;
A3: dom h = the carrier of T /\ the carrier of T by FUNCT_2:def_1
.= the carrier of T /\ (dom g) by FUNCT_2:def_1
.= (dom f) /\ (dom g) by FUNCT_2:def_1 ;
 for c being set st c in dom h holds
h . c = (f . c) + (g . c) by A1;
then  h = f + g by A3, VALUED_1:def_1;
hence  for b1 being RealMap of T st b1 = f + g holds
b1 is continuous by A2, JORDAN5A:27; ::_thesis: verum
end;
clusterf - g ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = f - g holds
b1 is continuous
proof
consider H being Function of T,R^1 such that
A4: for p being Point of T
for r1, r2 being real number st F . p = r1 & G . p = r2 holds
H . p = r1 - r2 and
A5: H is continuous by JGRAPH_2:21;
reconsider h = H as RealMap of T by TOPMETR:17;
A6: dom h = the carrier of T /\ the carrier of T by FUNCT_2:def_1
.= the carrier of T /\ (dom g) by FUNCT_2:def_1
.= (dom f) /\ (dom g) by FUNCT_2:def_1 ;
 ( dom (f - g) = (dom f) /\ (dom g) & ( for c being set st c in dom h holds
h . c = (f . c) - (g . c) ) ) by A4, VALUED_1:12;
then  h = f - g by A6, VALUED_1:14;
hence  for b1 being RealMap of T st b1 = f - g holds
b1 is continuous by A5, JORDAN5A:27; ::_thesis: verum
end;
clusterf (#) g ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = f (#) g holds
b1 is continuous
proof
consider H being Function of T,R^1 such that
A7: for p being Point of T
for r1, r2 being real number st F . p = r1 & G . p = r2 holds
H . p = r1 * r2 and
A8: H is continuous by JGRAPH_2:25;
reconsider h = H as RealMap of T by TOPMETR:17;
A9: dom h = the carrier of T /\ the carrier of T by FUNCT_2:def_1
.= the carrier of T /\ (dom g) by FUNCT_2:def_1
.= (dom f) /\ (dom g) by FUNCT_2:def_1 ;
 for c being set st c in dom h holds
h . c = (f . c) * (g . c) by A7;
then  h = f (#) g by A9, VALUED_1:def_4;
hence  for b1 being RealMap of T st b1 = f (#) g holds
b1 is continuous by A8, JORDAN5A:27; ::_thesis: verum
end;
end;

registration
let T be non empty TopSpace;
let f be continuous RealMap of T;
cluster - f ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = - f holds
b1 is continuous
proof
reconsider F = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17;
set c = the carrier of T;
consider H being Function of T,R^1 such that
A1: for p being Point of T
for r1 being real number st F . p = r1 holds
H . p = - r1 and
A2: H is continuous by JGRAPH_4:8;
reconsider h = H as RealMap of T by TOPMETR:17;
A3: dom h = the carrier of T by FUNCT_2:def_1
.= dom f by FUNCT_2:def_1 ;
 for c being set st c in dom h holds
h . c = - (f . c) by A1;
then  h = - f by A3, VALUED_1:9;
hence  for b1 being RealMap of T st b1 = - f holds
b1 is continuous by A2, JORDAN5A:27; ::_thesis: verum
end;
end;

registration
let T be non empty TopSpace;
let f be continuous RealMap of T;
cluster|.f.| ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = abs f holds
b1 is continuous
proof
reconsider F = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17;
set c = the carrier of T;
consider H being Function of T,R^1 such that
A1: for p being Point of T
for r1 being real number st F . p = r1 holds
H . p = abs r1 and
A2: H is continuous by JGRAPH_4:7;
reconsider h = H as RealMap of T by TOPMETR:17;
A3: dom h = the carrier of T by FUNCT_2:def_1
.= dom f by FUNCT_2:def_1 ;
 for c being set st c in dom h holds
h . c = abs (f . c) by A1;
then  h = abs f by A3, VALUED_1:def_11;
hence  for b1 being RealMap of T st b1 = abs f holds
b1 is continuous by A2, JORDAN5A:27; ::_thesis: verum
end;
end;

Lm1: now__::_thesis:_for_T_being_non_empty_TopSpace
for_a_being_Real_holds_the_carrier_of_T_-->_a_is_continuous
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
let Y be Subset of REAL; :: according to PSCOMP_1:def_3 ::_thesis: ( not Y is closed or ( the carrier of T --> a) " Y is closed )
A1: dom ( the carrier of T --> a) = the carrier of T by FUNCT_2:def_1;
assume  Y is closed ; ::_thesis: ( the carrier of T --> a) " Y is closed
A2: rng ( the carrier of T --> a) = {a} by FUNCOP_1:8;
percases ( 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:31;
( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:133
.= ( the carrier of T --> a) " (rng ( the carrier of T --> a)) by A3, XBOOLE_1:28
.= the carrier of T by A1, RELAT_1:134
.= [#] T ;
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:50;
( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:133
.= ( the carrier of T --> a) " {} by A4, XBOOLE_0:def_7
.= {} T ;
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 V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() continuous positive-yielding for Element of K6(K7( the carrier of T,REAL));
existence
 ex b1 being RealMap of T st
( b1 is positive-yielding & b1 is continuous )
proof
take f = the carrier of T --> 1; ::_thesis: ( f is positive-yielding & f is continuous )
thus  f is positive-yielding ; ::_thesis: f is continuous
thus  f is continuous by Lm1; ::_thesis: verum
end;
cluster non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() continuous negative-yielding for Element of K6(K7( the carrier of T,REAL));
existence
 ex b1 being RealMap of T st
( b1 is negative-yielding & b1 is continuous )
proof
take f = the carrier of T --> (- 1); ::_thesis: ( f is negative-yielding & f is continuous )
thus  f is negative-yielding ; ::_thesis: f is continuous
thus  f is continuous by Lm1; ::_thesis: verum
end;
end;

registration
let T be non empty TopSpace;
let f be continuous nonnegative-yielding RealMap of T;
cluster sqrt f ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = sqrt f holds
b1 is continuous
proof
reconsider F = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17;
set c = the carrier of T;
 for q being Point of T ex r being real number st
( f . q = r & r >= 0 )
proof
let q be Point of T; ::_thesis: ex r being real number st
( f . q = r & r >= 0 )
take  f . q ; ::_thesis: ( f . q = f . q & f . q >= 0 )
thus  f . q = f . q ; ::_thesis: f . q >= 0
 dom f = the carrier of T by FUNCT_2:def_1;
then  f . q in rng f by FUNCT_1:def_3;
hence  f . q >= 0 by PARTFUN3:def_4; ::_thesis: verum
end;
then consider H being Function of T,R^1 such that
A1: for p being Point of T
for r1 being real number st F . p = r1 holds
H . p = sqrt r1 and
A2: H is continuous by JGRAPH_3:5;
reconsider h = H as RealMap of T by TOPMETR:17;
A3: dom h = the carrier of T by FUNCT_2:def_1
.= dom f by FUNCT_2:def_1 ;
 for c being set st c in dom h holds
h . c = sqrt (f . c) by A1;
then  h = sqrt f by A3, PARTFUN3:def_5;
hence  for b1 being RealMap of T st b1 = sqrt f holds
b1 is continuous by A2, JORDAN5A:27; ::_thesis: verum
end;
end;

registration
let T be non empty TopSpace;
let f be continuous RealMap of T;
let r be real number ;
clusterr (#) f ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = r (#) f holds
b1 is continuous
proof
reconsider F = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17;
set c = the carrier of T;
consider H being Function of T,R^1 such that
A1: for p being Point of T
for r1 being real number st F . p = r1 holds
H . p = r * r1 and
A2: H is continuous by JGRAPH_2:23;
reconsider h = H as RealMap of T by TOPMETR:17;
A3: dom h = the carrier of T by FUNCT_2:def_1
.= dom f by FUNCT_2:def_1 ;
 for c being set st c in dom h holds
h . c = r * (f . c) by A1;
then  h = r (#) f by A3, VALUED_1:def_5;
hence  for b1 being RealMap of T st b1 = r (#) f holds
b1 is continuous by A2, JORDAN5A:27; ::_thesis: verum
end;
end;

registration
let T be non empty TopSpace;
let f be non-empty continuous RealMap of T;
clusterK498(f) ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = f ^ holds
b1 is continuous
proof
reconsider F = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17;
set c = the carrier of T;
 for q being Point of T holds f . q <> 0
proof
let q be Point of T; ::_thesis: f . q <> 0
 dom f = the carrier of T by FUNCT_2:def_1;
hence  f . q <> 0 ; ::_thesis: verum
end;
then consider H being Function of T,R^1 such that
A1: for p being Point of T
for r1 being real number st F . p = r1 holds
H . p = 1 / r1 and
A2: H is continuous by JGRAPH_2:26;
reconsider h = H as RealMap of T by TOPMETR:17;
A3: now__::_thesis:_for_a_being_set_st_a_in_dom_h_holds_
h_._a_=_(f_._a)_"
let a be set ; ::_thesis: ( a in dom h implies h . a = (f . a) " )
assume  a in dom h ; ::_thesis: h . a = (f . a) "
hence h . a = 1 / (f . a) by A1
.= 1 * ((f . a) ") by XCMPLX_0:def_9
.= (f . a) " ;
::_thesis: verum
end;
dom h = the carrier of T by FUNCT_2:def_1
.= (dom f) \ (f " {0}) by FUNCT_2:def_1 ;
then  h = f ^ by A3, RFUNCT_1:def_2;
hence  for b1 being RealMap of T st b1 = f ^ holds
b1 is continuous by A2, JORDAN5A:27; ::_thesis: verum
end;
end;

registration
let T be non empty TopSpace;
let f be continuous RealMap of T;
let g be non-empty continuous RealMap of T;
clusterK495(f,g) ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = f / g holds
b1 is continuous
proof
reconsider F = f, G = g as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17;
set c = the carrier of T;
 for q being Point of T holds g . q <> 0
proof
let q be Point of T; ::_thesis: g . q <> 0
 dom g = the carrier of T by FUNCT_2:def_1;
hence  g . q <> 0 ; ::_thesis: verum
end;
then consider H being Function of T,R^1 such that
A1: for p being Point of T
for r1, r2 being real number st F . p = r1 & G . p = r2 holds
H . p = r1 / r2 and
A2: H is continuous by JGRAPH_2:27;
reconsider h = H as RealMap of T by TOPMETR:17;
A3: now__::_thesis:_for_c_being_set_st_c_in_dom_h_holds_
h_._c_=_(f_._c)_*_((g_._c)_")
let c be set ; ::_thesis: ( c in dom h implies h . c = (f . c) * ((g . c) ") )
assume  c in dom h ; ::_thesis: h . c = (f . c) * ((g . c) ")
hence h . c = (f . c) / (g . c) by A1
.= (f . c) * ((g . c) ") by XCMPLX_0:def_9 ;
::_thesis: verum
end;
dom h = the carrier of T /\ the carrier of T by FUNCT_2:def_1
.= the carrier of T /\ (dom g) by FUNCT_2:def_1
.= (dom f) /\ ((dom g) \ (g " {0})) by FUNCT_2:def_1 ;
then  h = f / g by A3, RFUNCT_1:def_1;
hence  for b1 being RealMap of T st b1 = f / g holds
b1 is continuous by A2, JORDAN5A:27; ::_thesis: verum
end;
end;