:: RFUNCT_1 semantic presentation begin Lm1: (- 1) " = - 1 ; definition let f1, f2 be complex-valued Function; funcf1 / f2 -> Function means :Def1: :: RFUNCT_1:def 1 ( dom it = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom it holds it . c = (f1 . c) * ((f2 . c) ") ) ); existence ex b1 being Function st ( dom b1 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b1 holds b1 . c = (f1 . c) * ((f2 . c) ") ) ) proof deffunc H1( set ) -> set = (f1 . $1) * ((f2 . $1) "); ex f being Function st ( dom f = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for x being set st x in (dom f1) /\ ((dom f2) \ (f2 " {0})) holds f . x = H1(x) ) ) from FUNCT_1:sch_3(); hence ex b1 being Function st ( dom b1 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b1 holds b1 . c = (f1 . c) * ((f2 . c) ") ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b1 holds b1 . c = (f1 . c) * ((f2 . c) ") ) & dom b2 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b2 holds b2 . c = (f1 . c) * ((f2 . c) ") ) holds b1 = b2 proof let f, g be Function; ::_thesis: ( dom f = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom f holds f . c = (f1 . c) * ((f2 . c) ") ) & dom g = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom g holds g . c = (f1 . c) * ((f2 . c) ") ) implies f = g ) assume that A1: dom f = (dom f1) /\ ((dom f2) \ (f2 " {0})) and A2: for c being set st c in dom f holds f . c = (f1 . c) * ((f2 . c) ") and A3: dom g = (dom f1) /\ ((dom f2) \ (f2 " {0})) and A4: for c being set st c in dom g holds g . c = (f1 . c) * ((f2 . c) ") ; ::_thesis: f = g now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in dom f implies f . x = g . x ) assume A5: x in dom f ; ::_thesis: f . x = g . x hence f . x = (f1 . x) * ((f2 . x) ") by A2 .= g . x by A1, A3, A4, A5 ; ::_thesis: verum end; hence f = g by A1, A3, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def1 defines / RFUNCT_1:def_1_:_ for f1, f2 being complex-valued Function for b3 being Function holds ( b3 = f1 / f2 iff ( dom b3 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being set st c in dom b3 holds b3 . c = (f1 . c) * ((f2 . c) ") ) ) ); registration let f1, f2 be complex-valued Function; clusterf1 / f2 -> complex-valued ; coherence f1 / f2 is complex-valued proof let x be set ; :: according to VALUED_0:def_7 ::_thesis: ( not x in dom (f1 / f2) or (f1 / f2) . x is complex ) set F = f1 / f2; assume x in dom (f1 / f2) ; ::_thesis: (f1 / f2) . x is complex then (f1 / f2) . x = (f1 . x) * ((f2 . x) ") by Def1; hence (f1 / f2) . x is complex ; ::_thesis: verum end; end; registration let f1, f2 be real-valued Function; clusterf1 / f2 -> real-valued ; coherence f1 / f2 is real-valued proof let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (f1 / f2) or (f1 / f2) . x is real ) set F = f1 / f2; assume x in dom (f1 / f2) ; ::_thesis: (f1 / f2) . x is real then (f1 / f2) . x = (f1 . x) * ((f2 . x) ") by Def1; hence (f1 / f2) . x is real ; ::_thesis: verum end; end; definition let C be set ; let D be complex-membered set ; let f1, f2 be PartFunc of C,D; :: original: / redefine funcf1 / f2 -> PartFunc of C,COMPLEX; coherence f1 / f2 is PartFunc of C,COMPLEX proof set F = f1 / f2; A1: rng (f1 / f2) c= COMPLEX by VALUED_0:def_1; dom (f1 / f2) = (dom f1) /\ ((dom f2) \ (f2 " {0})) by Def1; hence f1 / f2 is PartFunc of C,COMPLEX by A1, RELSET_1:4; ::_thesis: verum end; end; definition let C be set ; let D be real-membered set ; let f1, f2 be PartFunc of C,D; :: original: / redefine funcf1 / f2 -> PartFunc of C,REAL; coherence f1 / f2 is PartFunc of C,REAL proof set F = f1 / f2; rng (f1 / f2) c= REAL by VALUED_0:def_3; then f1 / f2 is PartFunc of (dom (f1 / f2)),REAL by RELSET_1:4; hence f1 / f2 is PartFunc of C,REAL by RELSET_1:5; ::_thesis: verum end; end; definition let f be complex-valued Function; funcf ^ -> Function means :Def2: :: RFUNCT_1:def 2 ( dom it = (dom f) \ (f " {0}) & ( for c being set st c in dom it holds it . c = (f . c) " ) ); existence ex b1 being Function st ( dom b1 = (dom f) \ (f " {0}) & ( for c being set st c in dom b1 holds b1 . c = (f . c) " ) ) proof deffunc H1( set ) -> set = (f . $1) " ; ex h being Function st ( dom h = (dom f) \ (f " {0}) & ( for x being set st x in (dom f) \ (f " {0}) holds h . x = H1(x) ) ) from FUNCT_1:sch_3(); hence ex b1 being Function st ( dom b1 = (dom f) \ (f " {0}) & ( for c being set st c in dom b1 holds b1 . c = (f . c) " ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = (dom f) \ (f " {0}) & ( for c being set st c in dom b1 holds b1 . c = (f . c) " ) & dom b2 = (dom f) \ (f " {0}) & ( for c being set st c in dom b2 holds b2 . c = (f . c) " ) holds b1 = b2 proof let h, g be Function; ::_thesis: ( dom h = (dom f) \ (f " {0}) & ( for c being set st c in dom h holds h . c = (f . c) " ) & dom g = (dom f) \ (f " {0}) & ( for c being set st c in dom g holds g . c = (f . c) " ) implies h = g ) assume that A1: dom h = (dom f) \ (f " {0}) and A2: for c being set st c in dom h holds h . c = (f . c) " and A3: dom g = (dom f) \ (f " {0}) and A4: for c being set st c in dom g holds g . c = (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 = (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 Def2 defines ^ RFUNCT_1:def_2_:_ for f being complex-valued Function for b2 being Function holds ( b2 = f ^ iff ( dom b2 = (dom f) \ (f " {0}) & ( for c being set st c in dom b2 holds b2 . c = (f . c) " ) ) ); registration let f be complex-valued Function; clusterf ^ -> complex-valued ; coherence f ^ is complex-valued proof let x be set ; :: according to VALUED_0:def_7 ::_thesis: ( not x in dom (f ^) or (f ^) . x is complex ) set F = f ^ ; assume x in dom (f ^) ; ::_thesis: (f ^) . x is complex then (f ^) . x = (f . x) " by Def2; hence (f ^) . x is complex ; ::_thesis: verum end; end; registration let f be real-valued Function; clusterf ^ -> real-valued ; coherence f ^ is real-valued proof let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (f ^) or (f ^) . x is real ) set F = f ^ ; assume x in dom (f ^) ; ::_thesis: (f ^) . x is real then (f ^) . x = (f . x) " by Def2; hence (f ^) . x is real ; ::_thesis: verum end; end; definition let C be set ; let D be complex-membered set ; let f be PartFunc of C,D; :: original: ^ redefine funcf ^ -> PartFunc of C,COMPLEX; coherence f ^ is PartFunc of C,COMPLEX proof set F = f ^ ; A1: rng (f ^) c= COMPLEX by VALUED_0:def_1; dom (f ^) = (dom f) \ (f " {0}) by Def2; hence f ^ is PartFunc of C,COMPLEX by A1, RELSET_1:4; ::_thesis: verum end; end; definition let C be set ; let D be real-membered set ; let f be PartFunc of C,D; :: original: ^ redefine funcf ^ -> PartFunc of C,REAL; coherence f ^ is PartFunc of C,REAL proof set F = f ^ ; rng (f ^) c= REAL by VALUED_0:def_3; then f ^ is PartFunc of (dom (f ^)),REAL by RELSET_1:4; hence f ^ is PartFunc of C,REAL by RELSET_1:5; ::_thesis: verum end; end; theorem Th1: :: RFUNCT_1:1 for g being complex-valued Function holds ( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) ) proof let g be complex-valued Function; ::_thesis: ( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) ) dom (g ^) = (dom g) \ (g " {0}) by Def2; hence dom (g ^) c= dom g ; ::_thesis: (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) thus (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) by XBOOLE_1:28; ::_thesis: verum end; theorem Th2: :: RFUNCT_1:2 for f1, f2 being complex-valued Function holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) proof let f1, f2 be complex-valued Function; ::_thesis: (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) thus (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) c= ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) :: according to XBOOLE_0:def_10 ::_thesis: ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) or x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) ) assume A1: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) ; ::_thesis: x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) then not x in (f1 (#) f2) " {0} by XBOOLE_0:def_5; then not (f1 (#) f2) . x in {0} by A1, FUNCT_1:def_7; then (f1 (#) f2) . x <> 0 by TARSKI:def_1; then A2: (f1 . x) * (f2 . x) <> 0 by VALUED_1:5; then f2 . x <> 0 ; then not f2 . x in {0} by TARSKI:def_1; then A3: not x in f2 " {0} by FUNCT_1:def_7; x in dom (f1 (#) f2) by A1; then A4: x in (dom f1) /\ (dom f2) by VALUED_1:def_4; then x in dom f2 by XBOOLE_0:def_4; then A5: x in (dom f2) \ (f2 " {0}) by A3, XBOOLE_0:def_5; f1 . x <> 0 by A2; then not f1 . x in {0} by TARSKI:def_1; then A6: not x in f1 " {0} by FUNCT_1:def_7; x in dom f1 by A4, XBOOLE_0:def_4; then x in (dom f1) \ (f1 " {0}) by A6, XBOOLE_0:def_5; hence x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) by A5, XBOOLE_0:def_4; ::_thesis: verum end; thus ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) c= (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) or x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) ) assume A7: x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) ; ::_thesis: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) then x in (dom f2) \ (f2 " {0}) by XBOOLE_0:def_4; then not x in f2 " {0} by XBOOLE_0:def_5; then not f2 . x in {0} by A7, FUNCT_1:def_7; then A8: f2 . x <> 0 by TARSKI:def_1; A9: x in (dom f1) \ (f1 " {0}) by A7, XBOOLE_0:def_4; then not x in f1 " {0} by XBOOLE_0:def_5; then not f1 . x in {0} by A9, FUNCT_1:def_7; then f1 . x <> 0 by TARSKI:def_1; then (f1 . x) * (f2 . x) <> 0 by A8; then (f1 (#) f2) . x <> 0 by VALUED_1:5; then not (f1 (#) f2) . x in {0} by TARSKI:def_1; then A10: not x in (f1 (#) f2) " {0} by FUNCT_1:def_7; x in (dom f1) /\ (dom f2) by A7, A9, XBOOLE_0:def_4; then x in dom (f1 (#) f2) by VALUED_1:def_4; hence x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) by A10, XBOOLE_0:def_5; ::_thesis: verum end; end; theorem Th3: :: RFUNCT_1:3 for C being non empty set for c being Element of C for f being complex-valued Function st c in dom (f ^) holds f . c <> 0 proof let C be non empty set ; ::_thesis: for c being Element of C for f being complex-valued Function st c in dom (f ^) holds f . c <> 0 let c be Element of C; ::_thesis: for f being complex-valued Function st c in dom (f ^) holds f . c <> 0 let f be complex-valued Function; ::_thesis: ( c in dom (f ^) implies f . c <> 0 ) assume that A1: c in dom (f ^) and A2: f . c = 0 ; ::_thesis: contradiction A3: c in (dom f) \ (f " {0}) by A1, Def2; then A4: not c in f " {0} by XBOOLE_0:def_5; now__::_thesis:_contradiction percases ( not c in dom f or not f . c in {0} ) by A4, FUNCT_1:def_7; suppose not c in dom f ; ::_thesis: contradiction hence contradiction by A3; ::_thesis: verum end; suppose not f . c in {0} ; ::_thesis: contradiction hence contradiction by A2, TARSKI:def_1; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem Th4: :: RFUNCT_1:4 for f being complex-valued Function holds (f ^) " {0} = {} proof let f be complex-valued Function; ::_thesis: (f ^) " {0} = {} set x = the Element of (f ^) " {0}; assume A1: (f ^) " {0} <> {} ; ::_thesis: contradiction then A2: the Element of (f ^) " {0} in dom (f ^) by FUNCT_1:def_7; then A3: the Element of (f ^) " {0} in (dom f) \ (f " {0}) by Def2; then not the Element of (f ^) " {0} in f " {0} by XBOOLE_0:def_5; then A4: not f . the Element of (f ^) " {0} in {0} by A3, FUNCT_1:def_7; (f ^) . the Element of (f ^) " {0} in {0} by A1, FUNCT_1:def_7; then (f ^) . the Element of (f ^) " {0} = 0 by TARSKI:def_1; then (f . the Element of (f ^) " {0}) " = 0 by A2, Def2; hence contradiction by A4, TARSKI:def_1, XCMPLX_1:202; ::_thesis: verum end; theorem Th5: :: RFUNCT_1:5 for f being complex-valued Function holds ( (abs f) " {0} = f " {0} & (- f) " {0} = f " {0} ) proof let f be complex-valued Function; ::_thesis: ( (abs f) " {0} = f " {0} & (- f) " {0} = f " {0} ) now__::_thesis:_for_c_being_set_holds_ (_(_c_in_(abs_f)_"_{0}_implies_c_in_f_"_{0}_)_&_(_c_in_f_"_{0}_implies_c_in_(abs_f)_"_{0}_)_) let c be set ; ::_thesis: ( ( c in (abs f) " {0} implies c in f " {0} ) & ( c in f " {0} implies c in (abs f) " {0} ) ) thus ( c in (abs f) " {0} implies c in f " {0} ) ::_thesis: ( c in f " {0} implies c in (abs f) " {0} ) proof assume A1: c in (abs f) " {0} ; ::_thesis: c in f " {0} then (abs f) . c in {0} by FUNCT_1:def_7; then (abs f) . c = 0 by TARSKI:def_1; then abs (f . c) = 0 by VALUED_1:18; then f . c = 0 by COMPLEX1:45; then A2: f . c in {0} by TARSKI:def_1; c in dom (abs f) by A1, FUNCT_1:def_7; then c in dom f by VALUED_1:def_11; hence c in f " {0} by A2, FUNCT_1:def_7; ::_thesis: verum end; assume A3: c in f " {0} ; ::_thesis: c in (abs f) " {0} then f . c in {0} by FUNCT_1:def_7; then f . c = 0 by TARSKI:def_1; then abs (f . c) = 0 by ABSVALUE:2; then (abs f) . c = 0 by VALUED_1:18; then A4: (abs f) . c in {0} by TARSKI:def_1; c in dom f by A3, FUNCT_1:def_7; then c in dom (abs f) by VALUED_1:def_11; hence c in (abs f) " {0} by A4, FUNCT_1:def_7; ::_thesis: verum end; hence (abs f) " {0} = f " {0} by TARSKI:1; ::_thesis: (- f) " {0} = f " {0} now__::_thesis:_for_c_being_set_holds_ (_(_c_in_(-_f)_"_{0}_implies_c_in_f_"_{0}_)_&_(_c_in_f_"_{0}_implies_c_in_(-_f)_"_{0}_)_) let c be set ; ::_thesis: ( ( c in (- f) " {0} implies c in f " {0} ) & ( c in f " {0} implies c in (- f) " {0} ) ) thus ( c in (- f) " {0} implies c in f " {0} ) ::_thesis: ( c in f " {0} implies c in (- f) " {0} ) proof assume A5: c in (- f) " {0} ; ::_thesis: c in f " {0} then (- f) . c in {0} by FUNCT_1:def_7; then (- f) . c = 0 by TARSKI:def_1; then - (- (f . c)) = - 0 by VALUED_1:8; then A6: f . c in {0} by TARSKI:def_1; c in dom (- f) by A5, FUNCT_1:def_7; then c in dom f by VALUED_1:8; hence c in f " {0} by A6, FUNCT_1:def_7; ::_thesis: verum end; assume A7: c in f " {0} ; ::_thesis: c in (- f) " {0} then f . c in {0} by FUNCT_1:def_7; then f . c = 0 by TARSKI:def_1; then (- f) . c = - 0 by VALUED_1:8; then A8: (- f) . c in {0} by TARSKI:def_1; c in dom f by A7, FUNCT_1:def_7; then c in dom (- f) by VALUED_1:8; hence c in (- f) " {0} by A8, FUNCT_1:def_7; ::_thesis: verum end; hence (- f) " {0} = f " {0} by TARSKI:1; ::_thesis: verum end; theorem Th6: :: RFUNCT_1:6 for f being complex-valued Function holds dom ((f ^) ^) = dom (f | (dom (f ^))) proof let f be complex-valued Function; ::_thesis: dom ((f ^) ^) = dom (f | (dom (f ^))) A1: dom (f ^) = (dom f) \ (f " {0}) by Def2; thus dom ((f ^) ^) = (dom (f ^)) \ ((f ^) " {0}) by Def2 .= (dom (f ^)) \ {} by Th4 .= (dom f) /\ (dom (f ^)) by A1, XBOOLE_1:28 .= dom (f | (dom (f ^))) by RELAT_1:61 ; ::_thesis: verum end; theorem Th7: :: RFUNCT_1:7 for f being complex-valued Function for r being complex number st r <> 0 holds (r (#) f) " {0} = f " {0} proof let f be complex-valued Function; ::_thesis: for r being complex number st r <> 0 holds (r (#) f) " {0} = f " {0} let r be complex number ; ::_thesis: ( r <> 0 implies (r (#) f) " {0} = f " {0} ) assume A1: r <> 0 ; ::_thesis: (r (#) f) " {0} = f " {0} now__::_thesis:_for_c_being_set_holds_ (_(_c_in_(r_(#)_f)_"_{0}_implies_c_in_f_"_{0}_)_&_(_c_in_f_"_{0}_implies_c_in_(r_(#)_f)_"_{0}_)_) let c be set ; ::_thesis: ( ( c in (r (#) f) " {0} implies c in f " {0} ) & ( c in f " {0} implies c in (r (#) f) " {0} ) ) thus ( c in (r (#) f) " {0} implies c in f " {0} ) ::_thesis: ( c in f " {0} implies c in (r (#) f) " {0} ) proof assume A2: c in (r (#) f) " {0} ; ::_thesis: c in f " {0} then A3: c in dom (r (#) f) by FUNCT_1:def_7; (r (#) f) . c in {0} by A2, FUNCT_1:def_7; then (r (#) f) . c = 0 by TARSKI:def_1; then r * (f . c) = 0 by A3, VALUED_1:def_5; then f . c = 0 by A1; then A4: f . c in {0} by TARSKI:def_1; c in dom f by A3, VALUED_1:def_5; hence c in f " {0} by A4, FUNCT_1:def_7; ::_thesis: verum end; assume A5: c in f " {0} ; ::_thesis: c in (r (#) f) " {0} then f . c in {0} by FUNCT_1:def_7; then f . c = 0 by TARSKI:def_1; then A6: r * (f . c) = 0 ; A7: c in dom f by A5, FUNCT_1:def_7; then c in dom (r (#) f) by VALUED_1:def_5; then (r (#) f) . c = 0 by A6, VALUED_1:def_5; then A8: (r (#) f) . c in {0} by TARSKI:def_1; c in dom (r (#) f) by A7, VALUED_1:def_5; hence c in (r (#) f) " {0} by A8, FUNCT_1:def_7; ::_thesis: verum end; hence (r (#) f) " {0} = f " {0} by TARSKI:1; ::_thesis: verum end; theorem :: RFUNCT_1:8 for f1, f2, f3 being complex-valued Function holds (f1 + f2) + f3 = f1 + (f2 + f3) proof let f1, f2, f3 be complex-valued Function; ::_thesis: (f1 + f2) + f3 = f1 + (f2 + f3) A1: dom ((f1 + f2) + f3) = (dom (f1 + f2)) /\ (dom f3) by VALUED_1:def_1 .= ((dom f1) /\ (dom f2)) /\ (dom f3) by VALUED_1:def_1 .= (dom f1) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16 .= (dom f1) /\ (dom (f2 + f3)) by VALUED_1:def_1 .= dom (f1 + (f2 + f3)) by VALUED_1:def_1 ; now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_+_f2)_+_f3)_holds_ ((f1_+_f2)_+_f3)_._c_=_(f1_+_(f2_+_f3))_._c let c be set ; ::_thesis: ( c in dom ((f1 + f2) + f3) implies ((f1 + f2) + f3) . c = (f1 + (f2 + f3)) . c ) assume A2: c in dom ((f1 + f2) + f3) ; ::_thesis: ((f1 + f2) + f3) . c = (f1 + (f2 + f3)) . c then c in (dom (f1 + f2)) /\ (dom f3) by VALUED_1:def_1; then A3: c in dom (f1 + f2) by XBOOLE_0:def_4; c in (dom f1) /\ (dom (f2 + f3)) by A1, A2, VALUED_1:def_1; then A4: c in dom (f2 + f3) by XBOOLE_0:def_4; thus ((f1 + f2) + f3) . c = ((f1 + f2) . c) + (f3 . c) by A2, VALUED_1:def_1 .= ((f1 . c) + (f2 . c)) + (f3 . c) by A3, VALUED_1:def_1 .= (f1 . c) + ((f2 . c) + (f3 . c)) .= (f1 . c) + ((f2 + f3) . c) by A4, VALUED_1:def_1 .= (f1 + (f2 + f3)) . c by A1, A2, VALUED_1:def_1 ; ::_thesis: verum end; hence (f1 + f2) + f3 = f1 + (f2 + f3) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th9: :: RFUNCT_1:9 for f1, f2, f3 being complex-valued Function holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) proof let f1, f2, f3 be complex-valued Function; ::_thesis: (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_(#)_f2)_(#)_f3)_holds_ ((f1_(#)_f2)_(#)_f3)_._c_=_(f1_(#)_(f2_(#)_f3))_._c let c be set ; ::_thesis: ( c in dom ((f1 (#) f2) (#) f3) implies ((f1 (#) f2) (#) f3) . c = (f1 (#) (f2 (#) f3)) . c ) assume c in dom ((f1 (#) f2) (#) f3) ; ::_thesis: ((f1 (#) f2) (#) f3) . c = (f1 (#) (f2 (#) f3)) . c thus ((f1 (#) f2) (#) f3) . c = ((f1 (#) f2) . c) * (f3 . c) by VALUED_1:5 .= ((f1 . c) * (f2 . c)) * (f3 . c) by VALUED_1:5 .= (f1 . c) * ((f2 . c) * (f3 . c)) .= (f1 . c) * ((f2 (#) f3) . c) by VALUED_1:5 .= (f1 (#) (f2 (#) f3)) . c by VALUED_1:5 ; ::_thesis: verum end; dom ((f1 (#) f2) (#) f3) = (dom (f1 (#) f2)) /\ (dom f3) by VALUED_1:def_4 .= ((dom f1) /\ (dom f2)) /\ (dom f3) by VALUED_1:def_4 .= (dom f1) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16 .= (dom f1) /\ (dom (f2 (#) f3)) by VALUED_1:def_4 .= dom (f1 (#) (f2 (#) f3)) by VALUED_1:def_4 ; hence (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th10: :: RFUNCT_1:10 for f1, f2, f3 being complex-valued Function holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) proof let f1, f2, f3 be complex-valued Function; ::_thesis: (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) A1: dom ((f1 + f2) (#) f3) = (dom (f1 + f2)) /\ (dom f3) by VALUED_1:def_4 .= ((dom f1) /\ (dom f2)) /\ ((dom f3) /\ (dom f3)) by VALUED_1:def_1 .= (((dom f1) /\ (dom f2)) /\ (dom f3)) /\ (dom f3) by XBOOLE_1:16 .= (((dom f1) /\ (dom f3)) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16 .= ((dom f1) /\ (dom f3)) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16 .= (dom (f1 (#) f3)) /\ ((dom f2) /\ (dom f3)) by VALUED_1:def_4 .= (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by VALUED_1:def_4 .= dom ((f1 (#) f3) + (f2 (#) f3)) by VALUED_1:def_1 ; now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_+_f2)_(#)_f3)_holds_ ((f1_+_f2)_(#)_f3)_._c_=_((f1_(#)_f3)_+_(f2_(#)_f3))_._c let c be set ; ::_thesis: ( c in dom ((f1 + f2) (#) f3) implies ((f1 + f2) (#) f3) . c = ((f1 (#) f3) + (f2 (#) f3)) . c ) assume A2: c in dom ((f1 + f2) (#) f3) ; ::_thesis: ((f1 + f2) (#) f3) . c = ((f1 (#) f3) + (f2 (#) f3)) . c then c in (dom (f1 + f2)) /\ (dom f3) by VALUED_1:def_4; then A3: c in dom (f1 + f2) by XBOOLE_0:def_4; thus ((f1 + f2) (#) f3) . c = ((f1 + f2) . c) * (f3 . c) by VALUED_1:5 .= ((f1 . c) + (f2 . c)) * (f3 . c) by A3, VALUED_1:def_1 .= ((f1 . c) * (f3 . c)) + ((f2 . c) * (f3 . c)) .= ((f1 (#) f3) . c) + ((f2 . c) * (f3 . c)) by VALUED_1:5 .= ((f1 (#) f3) . c) + ((f2 (#) f3) . c) by VALUED_1:5 .= ((f1 (#) f3) + (f2 (#) f3)) . c by A1, A2, VALUED_1:def_1 ; ::_thesis: verum end; hence (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: RFUNCT_1:11 for f3, f1, f2 being complex-valued Function holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) by Th10; theorem Th12: :: RFUNCT_1:12 for f1, f2 being complex-valued Function for r being complex number holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2 proof let f1, f2 be complex-valued Function; ::_thesis: for r being complex number holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2 let r be complex number ; ::_thesis: r (#) (f1 (#) f2) = (r (#) f1) (#) f2 A1: dom (r (#) (f1 (#) f2)) = dom (f1 (#) f2) by VALUED_1:def_5 .= (dom f1) /\ (dom f2) by VALUED_1:def_4 .= (dom (r (#) f1)) /\ (dom f2) by VALUED_1:def_5 .= dom ((r (#) f1) (#) f2) by VALUED_1:def_4 ; now__::_thesis:_for_c_being_set_st_c_in_dom_(r_(#)_(f1_(#)_f2))_holds_ (r_(#)_(f1_(#)_f2))_._c_=_((r_(#)_f1)_(#)_f2)_._c let c be set ; ::_thesis: ( c in dom (r (#) (f1 (#) f2)) implies (r (#) (f1 (#) f2)) . c = ((r (#) f1) (#) f2) . c ) assume A2: c in dom (r (#) (f1 (#) f2)) ; ::_thesis: (r (#) (f1 (#) f2)) . c = ((r (#) f1) (#) f2) . c then c in (dom (r (#) f1)) /\ (dom f2) by A1, VALUED_1:def_4; then A3: c in dom (r (#) f1) by XBOOLE_0:def_4; thus (r (#) (f1 (#) f2)) . c = r * ((f1 (#) f2) . c) by A2, VALUED_1:def_5 .= r * ((f1 . c) * (f2 . c)) by VALUED_1:5 .= (r * (f1 . c)) * (f2 . c) .= ((r (#) f1) . c) * (f2 . c) by A3, VALUED_1:def_5 .= ((r (#) f1) (#) f2) . c by VALUED_1:5 ; ::_thesis: verum end; hence r (#) (f1 (#) f2) = (r (#) f1) (#) f2 by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th13: :: RFUNCT_1:13 for f1, f2 being complex-valued Function for r being complex number holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2) proof let f1, f2 be complex-valued Function; ::_thesis: for r being complex number holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2) let r be complex number ; ::_thesis: r (#) (f1 (#) f2) = f1 (#) (r (#) f2) A1: dom (r (#) (f1 (#) f2)) = dom (f1 (#) f2) by VALUED_1:def_5 .= (dom f1) /\ (dom f2) by VALUED_1:def_4 .= (dom f1) /\ (dom (r (#) f2)) by VALUED_1:def_5 .= dom (f1 (#) (r (#) f2)) by VALUED_1:def_4 ; now__::_thesis:_for_c_being_set_st_c_in_dom_(r_(#)_(f1_(#)_f2))_holds_ (r_(#)_(f1_(#)_f2))_._c_=_(f1_(#)_(r_(#)_f2))_._c let c be set ; ::_thesis: ( c in dom (r (#) (f1 (#) f2)) implies (r (#) (f1 (#) f2)) . c = (f1 (#) (r (#) f2)) . c ) assume A2: c in dom (r (#) (f1 (#) f2)) ; ::_thesis: (r (#) (f1 (#) f2)) . c = (f1 (#) (r (#) f2)) . c then c in (dom f1) /\ (dom (r (#) f2)) by A1, VALUED_1:def_4; then A3: c in dom (r (#) f2) by XBOOLE_0:def_4; thus (r (#) (f1 (#) f2)) . c = r * ((f1 (#) f2) . c) by A2, VALUED_1:def_5 .= r * ((f1 . c) * (f2 . c)) by VALUED_1:5 .= (f1 . c) * (r * (f2 . c)) .= (f1 . c) * ((r (#) f2) . c) by A3, VALUED_1:def_5 .= (f1 (#) (r (#) f2)) . c by VALUED_1:5 ; ::_thesis: verum end; hence r (#) (f1 (#) f2) = f1 (#) (r (#) f2) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th14: :: RFUNCT_1:14 for f1, f2, f3 being complex-valued Function holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) proof let f1, f2, f3 be complex-valued Function; ::_thesis: (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) A1: dom ((f1 - f2) (#) f3) = (dom (f1 - f2)) /\ (dom f3) by VALUED_1:def_4 .= ((dom f1) /\ (dom f2)) /\ ((dom f3) /\ (dom f3)) by VALUED_1:12 .= (((dom f1) /\ (dom f2)) /\ (dom f3)) /\ (dom f3) by XBOOLE_1:16 .= (((dom f1) /\ (dom f3)) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16 .= ((dom f1) /\ (dom f3)) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16 .= (dom (f1 (#) f3)) /\ ((dom f2) /\ (dom f3)) by VALUED_1:def_4 .= (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by VALUED_1:def_4 .= dom ((f1 (#) f3) - (f2 (#) f3)) by VALUED_1:12 ; now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_-_f2)_(#)_f3)_holds_ ((f1_-_f2)_(#)_f3)_._c_=_((f1_(#)_f3)_-_(f2_(#)_f3))_._c let c be set ; ::_thesis: ( c in dom ((f1 - f2) (#) f3) implies ((f1 - f2) (#) f3) . c = ((f1 (#) f3) - (f2 (#) f3)) . c ) assume A2: c in dom ((f1 - f2) (#) f3) ; ::_thesis: ((f1 - f2) (#) f3) . c = ((f1 (#) f3) - (f2 (#) f3)) . c then c in (dom (f1 - f2)) /\ (dom f3) by VALUED_1:def_4; then A3: c in dom (f1 - f2) by XBOOLE_0:def_4; thus ((f1 - f2) (#) f3) . c = ((f1 - f2) . c) * (f3 . c) by VALUED_1:5 .= ((f1 . c) - (f2 . c)) * (f3 . c) by A3, VALUED_1:13 .= ((f1 . c) * (f3 . c)) - ((f2 . c) * (f3 . c)) .= ((f1 (#) f3) . c) - ((f2 . c) * (f3 . c)) by VALUED_1:5 .= ((f1 (#) f3) . c) - ((f2 (#) f3) . c) by VALUED_1:5 .= ((f1 (#) f3) - (f2 (#) f3)) . c by A1, A2, VALUED_1:13 ; ::_thesis: verum end; hence (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: RFUNCT_1:15 for f3, f1, f2 being complex-valued Function holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) by Th14; theorem :: RFUNCT_1:16 for f1, f2 being complex-valued Function for r being complex number holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) proof let f1, f2 be complex-valued Function; ::_thesis: for r being complex number holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) let r be complex number ; ::_thesis: r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) A1: dom (r (#) (f1 + f2)) = dom (f1 + f2) by VALUED_1:def_5 .= (dom f1) /\ (dom f2) by VALUED_1:def_1 .= (dom f1) /\ (dom (r (#) f2)) by VALUED_1:def_5 .= (dom (r (#) f1)) /\ (dom (r (#) f2)) by VALUED_1:def_5 .= dom ((r (#) f1) + (r (#) f2)) by VALUED_1:def_1 ; now__::_thesis:_for_c_being_set_st_c_in_dom_(r_(#)_(f1_+_f2))_holds_ (r_(#)_(f1_+_f2))_._c_=_((r_(#)_f1)_+_(r_(#)_f2))_._c let c be set ; ::_thesis: ( c in dom (r (#) (f1 + f2)) implies (r (#) (f1 + f2)) . c = ((r (#) f1) + (r (#) f2)) . c ) assume A2: c in dom (r (#) (f1 + f2)) ; ::_thesis: (r (#) (f1 + f2)) . c = ((r (#) f1) + (r (#) f2)) . c then A3: c in dom (f1 + f2) by VALUED_1:def_5; A4: c in (dom (r (#) f1)) /\ (dom (r (#) f2)) by A1, A2, VALUED_1:def_1; then A5: c in dom (r (#) f1) by XBOOLE_0:def_4; A6: c in dom (r (#) f2) by A4, XBOOLE_0:def_4; thus (r (#) (f1 + f2)) . c = r * ((f1 + f2) . c) by A2, VALUED_1:def_5 .= r * ((f1 . c) + (f2 . c)) by A3, VALUED_1:def_1 .= (r * (f1 . c)) + (r * (f2 . c)) .= ((r (#) f1) . c) + (r * (f2 . c)) by A5, VALUED_1:def_5 .= ((r (#) f1) . c) + ((r (#) f2) . c) by A6, VALUED_1:def_5 .= ((r (#) f1) + (r (#) f2)) . c by A1, A2, VALUED_1:def_1 ; ::_thesis: verum end; hence r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: RFUNCT_1:17 for f being complex-valued Function for r, p being complex number holds (r * p) (#) f = r (#) (p (#) f) proof let f be complex-valued Function; ::_thesis: for r, p being complex number holds (r * p) (#) f = r (#) (p (#) f) let r, p be complex number ; ::_thesis: (r * p) (#) f = r (#) (p (#) f) A1: dom ((r * p) (#) f) = dom f by VALUED_1:def_5 .= dom (p (#) f) by VALUED_1:def_5 .= dom (r (#) (p (#) f)) by VALUED_1:def_5 ; now__::_thesis:_for_c_being_set_st_c_in_dom_((r_*_p)_(#)_f)_holds_ ((r_*_p)_(#)_f)_._c_=_(r_(#)_(p_(#)_f))_._c let c be set ; ::_thesis: ( c in dom ((r * p) (#) f) implies ((r * p) (#) f) . c = (r (#) (p (#) f)) . c ) assume A2: c in dom ((r * p) (#) f) ; ::_thesis: ((r * p) (#) f) . c = (r (#) (p (#) f)) . c then A3: c in dom (p (#) f) by A1, VALUED_1:def_5; thus ((r * p) (#) f) . c = (r * p) * (f . c) by A2, VALUED_1:def_5 .= r * (p * (f . c)) .= r * ((p (#) f) . c) by A3, VALUED_1:def_5 .= (r (#) (p (#) f)) . c by A1, A2, VALUED_1:def_5 ; ::_thesis: verum end; hence (r * p) (#) f = r (#) (p (#) f) by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: RFUNCT_1:18 for f1, f2 being complex-valued Function for r being complex number holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) proof let f1, f2 be complex-valued Function; ::_thesis: for r being complex number holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) let r be complex number ; ::_thesis: r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) A1: dom (r (#) (f1 - f2)) = dom (f1 - f2) by VALUED_1:def_5 .= (dom f1) /\ (dom f2) by VALUED_1:12 .= (dom f1) /\ (dom (r (#) f2)) by VALUED_1:def_5 .= (dom (r (#) f1)) /\ (dom (r (#) f2)) by VALUED_1:def_5 .= dom ((r (#) f1) - (r (#) f2)) by VALUED_1:12 ; now__::_thesis:_for_c_being_set_st_c_in_dom_(r_(#)_(f1_-_f2))_holds_ (r_(#)_(f1_-_f2))_._c_=_((r_(#)_f1)_-_(r_(#)_f2))_._c let c be set ; ::_thesis: ( c in dom (r (#) (f1 - f2)) implies (r (#) (f1 - f2)) . c = ((r (#) f1) - (r (#) f2)) . c ) assume A2: c in dom (r (#) (f1 - f2)) ; ::_thesis: (r (#) (f1 - f2)) . c = ((r (#) f1) - (r (#) f2)) . c then A3: c in dom (f1 - f2) by VALUED_1:def_5; A4: c in (dom (r (#) f1)) /\ (dom (r (#) f2)) by A1, A2, VALUED_1:12; then A5: c in dom (r (#) f1) by XBOOLE_0:def_4; A6: c in dom (r (#) f2) by A4, XBOOLE_0:def_4; thus (r (#) (f1 - f2)) . c = r * ((f1 - f2) . c) by A2, VALUED_1:def_5 .= r * ((f1 . c) - (f2 . c)) by A3, VALUED_1:13 .= (r * (f1 . c)) - (r * (f2 . c)) .= ((r (#) f1) . c) - (r * (f2 . c)) by A5, VALUED_1:def_5 .= ((r (#) f1) . c) - ((r (#) f2) . c) by A6, VALUED_1:def_5 .= ((r (#) f1) - (r (#) f2)) . c by A1, A2, VALUED_1:13 ; ::_thesis: verum end; hence r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: RFUNCT_1:19 for f1, f2 being complex-valued Function holds f1 - f2 = (- 1) (#) (f2 - f1) proof let f1, f2 be complex-valued Function; ::_thesis: f1 - f2 = (- 1) (#) (f2 - f1) A1: dom (f1 - f2) = (dom f2) /\ (dom f1) by VALUED_1:12 .= dom (f2 - f1) by VALUED_1:12 .= dom ((- 1) (#) (f2 - f1)) by VALUED_1:def_5 ; now__::_thesis:_for_c_being_set_st_c_in_dom_(f1_-_f2)_holds_ (f1_-_f2)_._c_=_((-_1)_(#)_(f2_-_f1))_._c A2: dom (f1 - f2) = (dom f2) /\ (dom f1) by VALUED_1:12 .= dom (f2 - f1) by VALUED_1:12 ; let c be set ; ::_thesis: ( c in dom (f1 - f2) implies (f1 - f2) . c = ((- 1) (#) (f2 - f1)) . c ) assume A3: c in dom (f1 - f2) ; ::_thesis: (f1 - f2) . c = ((- 1) (#) (f2 - f1)) . c thus (f1 - f2) . c = (f1 . c) - (f2 . c) by A3, VALUED_1:13 .= (- 1) * ((f2 . c) - (f1 . c)) .= (- 1) * ((f2 - f1) . c) by A3, A2, VALUED_1:13 .= ((- 1) (#) (f2 - f1)) . c by A1, A3, VALUED_1:def_5 ; ::_thesis: verum end; hence f1 - f2 = (- 1) (#) (f2 - f1) by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: RFUNCT_1:20 for f1, f2, f3 being complex-valued Function holds f1 - (f2 + f3) = (f1 - f2) - f3 proof let f1, f2, f3 be complex-valued Function; ::_thesis: f1 - (f2 + f3) = (f1 - f2) - f3 A1: dom (f1 - (f2 + f3)) = (dom f1) /\ (dom (f2 + f3)) by VALUED_1:12 .= (dom f1) /\ ((dom f2) /\ (dom f3)) by VALUED_1:def_1 .= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16 .= (dom (f1 - f2)) /\ (dom f3) by VALUED_1:12 .= dom ((f1 - f2) - f3) by VALUED_1:12 ; now__::_thesis:_for_c_being_set_st_c_in_dom_(f1_-_(f2_+_f3))_holds_ (f1_-_(f2_+_f3))_._c_=_((f1_-_f2)_-_f3)_._c let c be set ; ::_thesis: ( c in dom (f1 - (f2 + f3)) implies (f1 - (f2 + f3)) . c = ((f1 - f2) - f3) . c ) assume A2: c in dom (f1 - (f2 + f3)) ; ::_thesis: (f1 - (f2 + f3)) . c = ((f1 - f2) - f3) . c then c in (dom f1) /\ (dom (f2 + f3)) by VALUED_1:12; then A3: c in dom (f2 + f3) by XBOOLE_0:def_4; c in (dom (f1 - f2)) /\ (dom f3) by A1, A2, VALUED_1:12; then A4: c in dom (f1 - f2) by XBOOLE_0:def_4; thus (f1 - (f2 + f3)) . c = (f1 . c) - ((f2 + f3) . c) by A2, VALUED_1:13 .= (f1 . c) - ((f2 . c) + (f3 . c)) by A3, VALUED_1:def_1 .= ((f1 . c) - (f2 . c)) - (f3 . c) .= ((f1 - f2) . c) - (f3 . c) by A4, VALUED_1:13 .= ((f1 - f2) - f3) . c by A1, A2, VALUED_1:13 ; ::_thesis: verum end; hence f1 - (f2 + f3) = (f1 - f2) - f3 by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: RFUNCT_1:21 for f being complex-valued Function holds 1 (#) f = f proof let f be complex-valued Function; ::_thesis: 1 (#) f = f A1: now__::_thesis:_for_c_being_set_st_c_in_dom_(1_(#)_f)_holds_ (1_(#)_f)_._c_=_f_._c let c be set ; ::_thesis: ( c in dom (1 (#) f) implies (1 (#) f) . c = f . c ) assume c in dom (1 (#) f) ; ::_thesis: (1 (#) f) . c = f . c hence (1 (#) f) . c = 1 * (f . c) by VALUED_1:def_5 .= f . c ; ::_thesis: verum end; dom (1 (#) f) = dom f by VALUED_1:def_5; hence 1 (#) f = f by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: RFUNCT_1:22 for f1, f2, f3 being complex-valued Function holds f1 - (f2 - f3) = (f1 - f2) + f3 proof let f1, f2, f3 be complex-valued Function; ::_thesis: f1 - (f2 - f3) = (f1 - f2) + f3 A1: dom (f1 - (f2 - f3)) = (dom f1) /\ (dom (f2 - f3)) by VALUED_1:12 .= (dom f1) /\ ((dom f2) /\ (dom f3)) by VALUED_1:12 .= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16 .= (dom (f1 - f2)) /\ (dom f3) by VALUED_1:12 .= dom ((f1 - f2) + f3) by VALUED_1:def_1 ; now__::_thesis:_for_c_being_set_st_c_in_dom_(f1_-_(f2_-_f3))_holds_ (f1_-_(f2_-_f3))_._c_=_((f1_-_f2)_+_f3)_._c let c be set ; ::_thesis: ( c in dom (f1 - (f2 - f3)) implies (f1 - (f2 - f3)) . c = ((f1 - f2) + f3) . c ) assume A2: c in dom (f1 - (f2 - f3)) ; ::_thesis: (f1 - (f2 - f3)) . c = ((f1 - f2) + f3) . c then c in (dom f1) /\ (dom (f2 - f3)) by VALUED_1:12; then A3: c in dom (f2 - f3) by XBOOLE_0:def_4; c in (dom (f1 - f2)) /\ (dom f3) by A1, A2, VALUED_1:def_1; then A4: c in dom (f1 - f2) by XBOOLE_0:def_4; thus (f1 - (f2 - f3)) . c = (f1 . c) - ((f2 - f3) . c) by A2, VALUED_1:13 .= (f1 . c) - ((f2 . c) - (f3 . c)) by A3, VALUED_1:13 .= ((f1 . c) - (f2 . c)) + (f3 . c) .= ((f1 - f2) . c) + (f3 . c) by A4, VALUED_1:13 .= ((f1 - f2) + f3) . c by A1, A2, VALUED_1:def_1 ; ::_thesis: verum end; hence f1 - (f2 - f3) = (f1 - f2) + f3 by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: RFUNCT_1:23 for f1, f2, f3 being complex-valued Function holds f1 + (f2 - f3) = (f1 + f2) - f3 proof let f1, f2, f3 be complex-valued Function; ::_thesis: f1 + (f2 - f3) = (f1 + f2) - f3 A1: dom (f1 + (f2 - f3)) = (dom f1) /\ (dom (f2 - f3)) by VALUED_1:def_1 .= (dom f1) /\ ((dom f2) /\ (dom f3)) by VALUED_1:12 .= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16 .= (dom (f1 + f2)) /\ (dom f3) by VALUED_1:def_1 .= dom ((f1 + f2) - f3) by VALUED_1:12 ; now__::_thesis:_for_c_being_set_st_c_in_dom_(f1_+_(f2_-_f3))_holds_ (f1_+_(f2_-_f3))_._c_=_((f1_+_f2)_-_f3)_._c let c be set ; ::_thesis: ( c in dom (f1 + (f2 - f3)) implies (f1 + (f2 - f3)) . c = ((f1 + f2) - f3) . c ) assume A2: c in dom (f1 + (f2 - f3)) ; ::_thesis: (f1 + (f2 - f3)) . c = ((f1 + f2) - f3) . c then c in (dom f1) /\ (dom (f2 - f3)) by VALUED_1:def_1; then A3: c in dom (f2 - f3) by XBOOLE_0:def_4; c in (dom (f1 + f2)) /\ (dom f3) by A1, A2, VALUED_1:12; then A4: c in dom (f1 + f2) by XBOOLE_0:def_4; thus (f1 + (f2 - f3)) . c = (f1 . c) + ((f2 - f3) . c) by A2, VALUED_1:def_1 .= (f1 . c) + ((f2 . c) - (f3 . c)) by A3, VALUED_1:13 .= ((f1 . c) + (f2 . c)) - (f3 . c) .= ((f1 + f2) . c) - (f3 . c) by A4, VALUED_1:def_1 .= ((f1 + f2) - f3) . c by A1, A2, VALUED_1:13 ; ::_thesis: verum end; hence f1 + (f2 - f3) = (f1 + f2) - f3 by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th24: :: RFUNCT_1:24 for f1, f2 being complex-valued Function holds abs (f1 (#) f2) = (abs f1) (#) (abs f2) proof let f1, f2 be complex-valued Function; ::_thesis: abs (f1 (#) f2) = (abs f1) (#) (abs f2) A1: now__::_thesis:_for_c_being_set_st_c_in_dom_(abs_(f1_(#)_f2))_holds_ (abs_(f1_(#)_f2))_._c_=_((abs_f1)_(#)_(abs_f2))_._c let c be set ; ::_thesis: ( c in dom (abs (f1 (#) f2)) implies (abs (f1 (#) f2)) . c = ((abs f1) (#) (abs f2)) . c ) assume c in dom (abs (f1 (#) f2)) ; ::_thesis: (abs (f1 (#) f2)) . c = ((abs f1) (#) (abs f2)) . c thus (abs (f1 (#) f2)) . c = abs ((f1 (#) f2) . c) by VALUED_1:18 .= abs ((f1 . c) * (f2 . c)) by VALUED_1:5 .= (abs (f1 . c)) * (abs (f2 . c)) by COMPLEX1:65 .= ((abs f1) . c) * (abs (f2 . c)) by VALUED_1:18 .= ((abs f1) . c) * ((abs f2) . c) by VALUED_1:18 .= ((abs f1) (#) (abs f2)) . c by VALUED_1:5 ; ::_thesis: verum end; dom (abs (f1 (#) f2)) = dom (f1 (#) f2) by VALUED_1:def_11 .= (dom f1) /\ (dom f2) by VALUED_1:def_4 .= (dom f1) /\ (dom (abs f2)) by VALUED_1:def_11 .= (dom (abs f1)) /\ (dom (abs f2)) by VALUED_1:def_11 .= dom ((abs f1) (#) (abs f2)) by VALUED_1:def_4 ; hence abs (f1 (#) f2) = (abs f1) (#) (abs f2) by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: RFUNCT_1:25 for f being complex-valued Function for r being complex number holds abs (r (#) f) = (abs r) (#) (abs f) proof let f be complex-valued Function; ::_thesis: for r being complex number holds abs (r (#) f) = (abs r) (#) (abs f) let r be complex number ; ::_thesis: abs (r (#) f) = (abs r) (#) (abs f) A1: dom (abs (r (#) f)) = dom (r (#) f) by VALUED_1:def_11 .= dom f by VALUED_1:def_5 .= dom (abs f) by VALUED_1:def_11 .= dom ((abs r) (#) (abs f)) by VALUED_1:def_5 ; now__::_thesis:_for_c_being_set_st_c_in_dom_(abs_(r_(#)_f))_holds_ (abs_(r_(#)_f))_._c_=_((abs_r)_(#)_(abs_f))_._c let c be set ; ::_thesis: ( c in dom (abs (r (#) f)) implies (abs (r (#) f)) . c = ((abs r) (#) (abs f)) . c ) assume A2: c in dom (abs (r (#) f)) ; ::_thesis: (abs (r (#) f)) . c = ((abs r) (#) (abs f)) . c then A3: c in dom (r (#) f) by VALUED_1:def_11; thus (abs (r (#) f)) . c = abs ((r (#) f) . c) by VALUED_1:18 .= abs (r * (f . c)) by A3, VALUED_1:def_5 .= (abs r) * (abs (f . c)) by COMPLEX1:65 .= (abs r) * ((abs f) . c) by VALUED_1:18 .= ((abs r) (#) (abs f)) . c by A1, A2, VALUED_1:def_5 ; ::_thesis: verum end; hence abs (r (#) f) = (abs r) (#) (abs f) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th26: :: RFUNCT_1:26 for f being complex-valued Function holds (f ^) ^ = f | (dom (f ^)) proof let f be complex-valued Function; ::_thesis: (f ^) ^ = f | (dom (f ^)) A1: dom ((f ^) ^) = dom (f | (dom (f ^))) by Th6; now__::_thesis:_for_c_being_set_st_c_in_dom_((f_^)_^)_holds_ ((f_^)_^)_._c_=_(f_|_(dom_(f_^)))_._c let c be set ; ::_thesis: ( c in dom ((f ^) ^) implies ((f ^) ^) . c = (f | (dom (f ^))) . c ) assume A2: c in dom ((f ^) ^) ; ::_thesis: ((f ^) ^) . c = (f | (dom (f ^))) . c then c in (dom f) /\ (dom (f ^)) by A1, RELAT_1:61; then A3: c in dom (f ^) by XBOOLE_0:def_4; thus ((f ^) ^) . c = ((f ^) . c) " by A2, Def2 .= ((f . c) ") " by A3, Def2 .= (f | (dom (f ^))) . c by A1, A2, FUNCT_1:47 ; ::_thesis: verum end; hence (f ^) ^ = f | (dom (f ^)) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th27: :: RFUNCT_1:27 for f1, f2 being complex-valued Function holds (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^) proof let f1, f2 be complex-valued Function; ::_thesis: (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^) A1: dom ((f1 (#) f2) ^) = (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) by Def2 .= ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) by Th2 .= (dom (f1 ^)) /\ ((dom f2) \ (f2 " {0})) by Def2 .= (dom (f1 ^)) /\ (dom (f2 ^)) by Def2 .= dom ((f1 ^) (#) (f2 ^)) by VALUED_1:def_4 ; now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_(#)_f2)_^)_holds_ ((f1_(#)_f2)_^)_._c_=_((f1_^)_(#)_(f2_^))_._c let c be set ; ::_thesis: ( c in dom ((f1 (#) f2) ^) implies ((f1 (#) f2) ^) . c = ((f1 ^) (#) (f2 ^)) . c ) assume A2: c in dom ((f1 (#) f2) ^) ; ::_thesis: ((f1 (#) f2) ^) . c = ((f1 ^) (#) (f2 ^)) . c then A3: c in (dom (f1 ^)) /\ (dom (f2 ^)) by A1, VALUED_1:def_4; then A4: c in dom (f1 ^) by XBOOLE_0:def_4; A5: c in dom (f2 ^) by A3, XBOOLE_0:def_4; thus ((f1 (#) f2) ^) . c = ((f1 (#) f2) . c) " by A2, Def2 .= ((f1 . c) * (f2 . c)) " by VALUED_1:5 .= ((f1 . c) ") * ((f2 . c) ") by XCMPLX_1:204 .= ((f1 ^) . c) * ((f2 . c) ") by A4, Def2 .= ((f1 ^) . c) * ((f2 ^) . c) by A5, Def2 .= ((f1 ^) (#) (f2 ^)) . c by VALUED_1:5 ; ::_thesis: verum end; hence (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th28: :: RFUNCT_1:28 for f being complex-valued Function for r being complex number st r <> 0 holds (r (#) f) ^ = (r ") (#) (f ^) proof let f be complex-valued Function; ::_thesis: for r being complex number st r <> 0 holds (r (#) f) ^ = (r ") (#) (f ^) let r be complex number ; ::_thesis: ( r <> 0 implies (r (#) f) ^ = (r ") (#) (f ^) ) assume A1: r <> 0 ; ::_thesis: (r (#) f) ^ = (r ") (#) (f ^) A2: dom ((r (#) f) ^) = (dom (r (#) f)) \ ((r (#) f) " {0}) by Def2 .= (dom (r (#) f)) \ (f " {0}) by A1, Th7 .= (dom f) \ (f " {0}) by VALUED_1:def_5 .= dom (f ^) by Def2 .= dom ((r ") (#) (f ^)) by VALUED_1:def_5 ; now__::_thesis:_for_c_being_set_st_c_in_dom_((r_(#)_f)_^)_holds_ ((r_(#)_f)_^)_._c_=_((r_")_(#)_(f_^))_._c let c be set ; ::_thesis: ( c in dom ((r (#) f) ^) implies ((r (#) f) ^) . c = ((r ") (#) (f ^)) . c ) assume A3: c in dom ((r (#) f) ^) ; ::_thesis: ((r (#) f) ^) . c = ((r ") (#) (f ^)) . c then A4: c in (dom (r (#) f)) \ ((r (#) f) " {0}) by Def2; A5: c in dom (f ^) by A2, A3, VALUED_1:def_5; thus ((r (#) f) ^) . c = ((r (#) f) . c) " by A3, Def2 .= (r * (f . c)) " by A4, VALUED_1:def_5 .= (r ") * ((f . c) ") by XCMPLX_1:204 .= (r ") * ((f ^) . c) by A5, Def2 .= ((r ") (#) (f ^)) . c by A2, A3, VALUED_1:def_5 ; ::_thesis: verum end; hence (r (#) f) ^ = (r ") (#) (f ^) by A2, FUNCT_1:2; ::_thesis: verum end; theorem :: RFUNCT_1:29 for f being complex-valued Function holds (- f) ^ = (- 1) (#) (f ^) by Lm1, Th28; theorem Th30: :: RFUNCT_1:30 for f being complex-valued Function holds (abs f) ^ = abs (f ^) proof let f be complex-valued Function; ::_thesis: (abs f) ^ = abs (f ^) A1: dom ((abs f) ^) = (dom (abs f)) \ ((abs f) " {0}) by Def2 .= (dom f) \ ((abs f) " {0}) by VALUED_1:def_11 .= (dom f) \ (f " {0}) by Th5 .= dom (f ^) by Def2 .= dom (abs (f ^)) by VALUED_1:def_11 ; now__::_thesis:_for_c_being_set_st_c_in_dom_((abs_f)_^)_holds_ ((abs_f)_^)_._c_=_(abs_(f_^))_._c let c be set ; ::_thesis: ( c in dom ((abs f) ^) implies ((abs f) ^) . c = (abs (f ^)) . c ) assume A2: c in dom ((abs f) ^) ; ::_thesis: ((abs f) ^) . c = (abs (f ^)) . c then A3: c in dom (f ^) by A1, VALUED_1:def_11; thus ((abs f) ^) . c = ((abs f) . c) " by A2, Def2 .= (abs (f . c)) " by VALUED_1:18 .= 1 / (abs (f . c)) by XCMPLX_1:215 .= abs (1 / (f . c)) by COMPLEX1:80 .= abs ((f . c) ") by XCMPLX_1:215 .= abs ((f ^) . c) by A3, Def2 .= (abs (f ^)) . c by VALUED_1:18 ; ::_thesis: verum end; hence (abs f) ^ = abs (f ^) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th31: :: RFUNCT_1:31 for f, g being complex-valued Function holds f / g = f (#) (g ^) proof let f, g be complex-valued Function; ::_thesis: f / g = f (#) (g ^) A1: now__::_thesis:_for_c_being_set_st_c_in_dom_(f_/_g)_holds_ (f_/_g)_._c_=_(f_(#)_(g_^))_._c let c be set ; ::_thesis: ( c in dom (f / g) implies (f / g) . c = (f (#) (g ^)) . c ) assume A2: c in dom (f / g) ; ::_thesis: (f / g) . c = (f (#) (g ^)) . c then c in (dom f) /\ ((dom g) \ (g " {0})) by Def1; then c in (dom f) /\ (dom (g ^)) by Def2; then A3: c in dom (g ^) by XBOOLE_0:def_4; thus (f / g) . c = (f . c) * ((g . c) ") by A2, Def1 .= (f . c) * ((g ^) . c) by A3, Def2 .= (f (#) (g ^)) . c by VALUED_1:5 ; ::_thesis: verum end; dom (f / g) = (dom f) /\ ((dom g) \ (g " {0})) by Def1 .= (dom f) /\ (dom (g ^)) by Def2 .= dom (f (#) (g ^)) by VALUED_1:def_4 ; hence f / g = f (#) (g ^) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th32: :: RFUNCT_1:32 for g, f being complex-valued Function for r being complex number holds r (#) (g / f) = (r (#) g) / f proof let g, f be complex-valued Function; ::_thesis: for r being complex number holds r (#) (g / f) = (r (#) g) / f let r be complex number ; ::_thesis: r (#) (g / f) = (r (#) g) / f thus r (#) (g / f) = r (#) (g (#) (f ^)) by Th31 .= (r (#) g) (#) (f ^) by Th12 .= (r (#) g) / f by Th31 ; ::_thesis: verum end; theorem :: RFUNCT_1:33 for f, g being complex-valued Function holds (f / g) (#) g = f | (dom (g ^)) proof let f, g be complex-valued Function; ::_thesis: (f / g) (#) g = f | (dom (g ^)) A1: dom ((f / g) (#) g) = (dom (f / g)) /\ (dom g) by VALUED_1:def_4 .= ((dom f) /\ ((dom g) \ (g " {0}))) /\ (dom g) by Def1 .= (dom f) /\ (((dom g) \ (g " {0})) /\ (dom g)) by XBOOLE_1:16 .= (dom f) /\ ((dom (g ^)) /\ (dom g)) by Def2 .= (dom f) /\ (dom (g ^)) by Th1, XBOOLE_1:28 .= dom (f | (dom (g ^))) by RELAT_1:61 ; now__::_thesis:_for_c_being_set_st_c_in_dom_((f_/_g)_(#)_g)_holds_ ((f_/_g)_(#)_g)_._c_=_(f_|_(dom_(g_^)))_._c let c be set ; ::_thesis: ( c in dom ((f / g) (#) g) implies ((f / g) (#) g) . c = (f | (dom (g ^))) . c ) assume A2: c in dom ((f / g) (#) g) ; ::_thesis: ((f / g) (#) g) . c = (f | (dom (g ^))) . c then c in (dom f) /\ (dom (g ^)) by A1, RELAT_1:61; then A3: c in dom (g ^) by XBOOLE_0:def_4; then A4: g . c <> 0 by Th3; thus ((f / g) (#) g) . c = ((f / g) . c) * (g . c) by VALUED_1:5 .= ((f (#) (g ^)) . c) * (g . c) by Th31 .= ((f . c) * ((g ^) . c)) * (g . c) by VALUED_1:5 .= ((f . c) * ((g . c) ")) * (g . c) by A3, Def2 .= (f . c) * (((g . c) ") * (g . c)) .= (f . c) * 1 by A4, XCMPLX_0:def_7 .= (f | (dom (g ^))) . c by A1, A2, FUNCT_1:47 ; ::_thesis: verum end; hence (f / g) (#) g = f | (dom (g ^)) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th34: :: RFUNCT_1:34 for f, g, f1, g1 being complex-valued Function holds (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1) proof let f, g, f1, g1 be complex-valued Function; ::_thesis: (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1) A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((f_/_g)_(#)_(f1_/_g1))_holds_ ((f_/_g)_(#)_(f1_/_g1))_._c_=_((f_(#)_f1)_/_(g_(#)_g1))_._c let c be set ; ::_thesis: ( c in dom ((f / g) (#) (f1 / g1)) implies ((f / g) (#) (f1 / g1)) . c = ((f (#) f1) / (g (#) g1)) . c ) assume c in dom ((f / g) (#) (f1 / g1)) ; ::_thesis: ((f / g) (#) (f1 / g1)) . c = ((f (#) f1) / (g (#) g1)) . c thus ((f / g) (#) (f1 / g1)) . c = ((f / g) . c) * ((f1 / g1) . c) by VALUED_1:5 .= ((f (#) (g ^)) . c) * ((f1 / g1) . c) by Th31 .= ((f (#) (g ^)) . c) * ((f1 (#) (g1 ^)) . c) by Th31 .= ((f . c) * ((g ^) . c)) * ((f1 (#) (g1 ^)) . c) by VALUED_1:5 .= ((f . c) * ((g ^) . c)) * ((f1 . c) * ((g1 ^) . c)) by VALUED_1:5 .= (f . c) * ((f1 . c) * (((g ^) . c) * ((g1 ^) . c))) .= (f . c) * ((f1 . c) * (((g ^) (#) (g1 ^)) . c)) by VALUED_1:5 .= ((f . c) * (f1 . c)) * (((g ^) (#) (g1 ^)) . c) .= ((f . c) * (f1 . c)) * (((g (#) g1) ^) . c) by Th27 .= ((f (#) f1) . c) * (((g (#) g1) ^) . c) by VALUED_1:5 .= ((f (#) f1) (#) ((g (#) g1) ^)) . c by VALUED_1:5 .= ((f (#) f1) / (g (#) g1)) . c by Th31 ; ::_thesis: verum end; dom ((f / g) (#) (f1 / g1)) = (dom (f / g)) /\ (dom (f1 / g1)) by VALUED_1:def_4 .= ((dom f) /\ ((dom g) \ (g " {0}))) /\ (dom (f1 / g1)) by Def1 .= ((dom f) /\ ((dom g) \ (g " {0}))) /\ ((dom f1) /\ ((dom g1) \ (g1 " {0}))) by Def1 .= (dom f) /\ (((dom g) \ (g " {0})) /\ ((dom f1) /\ ((dom g1) \ (g1 " {0})))) by XBOOLE_1:16 .= (dom f) /\ ((dom f1) /\ (((dom g) \ (g " {0})) /\ ((dom g1) \ (g1 " {0})))) by XBOOLE_1:16 .= ((dom f) /\ (dom f1)) /\ (((dom g) \ (g " {0})) /\ ((dom g1) \ (g1 " {0}))) by XBOOLE_1:16 .= (dom (f (#) f1)) /\ (((dom g) \ (g " {0})) /\ ((dom g1) \ (g1 " {0}))) by VALUED_1:def_4 .= (dom (f (#) f1)) /\ ((dom (g (#) g1)) \ ((g (#) g1) " {0})) by Th2 .= dom ((f (#) f1) / (g (#) g1)) by Def1 ; hence (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th35: :: RFUNCT_1:35 for f1, f2 being complex-valued Function holds (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1 proof let f1, f2 be complex-valued Function; ::_thesis: (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1 thus (f1 / f2) ^ = (f1 (#) (f2 ^)) ^ by Th31 .= (f1 ^) (#) ((f2 ^) ^) by Th27 .= (f2 | (dom (f2 ^))) (#) (f1 ^) by Th26 .= (f2 | (dom (f2 ^))) / f1 by Th31 ; ::_thesis: verum end; theorem Th36: :: RFUNCT_1:36 for g, f1, f2 being complex-valued Function holds g (#) (f1 / f2) = (g (#) f1) / f2 proof let g, f1, f2 be complex-valued Function; ::_thesis: g (#) (f1 / f2) = (g (#) f1) / f2 thus g (#) (f1 / f2) = g (#) (f1 (#) (f2 ^)) by Th31 .= (g (#) f1) (#) (f2 ^) by Th9 .= (g (#) f1) / f2 by Th31 ; ::_thesis: verum end; theorem :: RFUNCT_1:37 for g, f1, f2 being complex-valued Function holds g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1 proof let g, f1, f2 be complex-valued Function; ::_thesis: g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1 thus g / (f1 / f2) = g (#) ((f1 / f2) ^) by Th31 .= g (#) ((f2 | (dom (f2 ^))) / f1) by Th35 .= (g (#) (f2 | (dom (f2 ^)))) / f1 by Th36 ; ::_thesis: verum end; theorem :: RFUNCT_1:38 for f, g being complex-valued Function holds ( - (f / g) = (- f) / g & f / (- g) = - (f / g) ) proof let f, g be complex-valued Function; ::_thesis: ( - (f / g) = (- f) / g & f / (- g) = - (f / g) ) thus - (f / g) = (- f) / g by Th32; ::_thesis: f / (- g) = - (f / g) thus f / (- g) = f (#) ((- g) ^) by Th31 .= f (#) ((- 1) (#) (g ^)) by Lm1, Th28 .= - (f (#) (g ^)) by Th13 .= - (f / g) by Th31 ; ::_thesis: verum end; theorem :: RFUNCT_1:39 for f1, f, f2 being complex-valued Function holds ( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f ) proof let f1, f, f2 be complex-valued Function; ::_thesis: ( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f ) thus (f1 / f) + (f2 / f) = (f1 (#) (f ^)) + (f2 / f) by Th31 .= (f1 (#) (f ^)) + (f2 (#) (f ^)) by Th31 .= (f1 + f2) (#) (f ^) by Th10 .= (f1 + f2) / f by Th31 ; ::_thesis: (f1 / f) - (f2 / f) = (f1 - f2) / f thus (f1 / f) - (f2 / f) = (f1 (#) (f ^)) - (f2 / f) by Th31 .= (f1 (#) (f ^)) - (f2 (#) (f ^)) by Th31 .= (f1 - f2) (#) (f ^) by Th14 .= (f1 - f2) / f by Th31 ; ::_thesis: verum end; theorem Th40: :: RFUNCT_1:40 for f1, f, g1, g being complex-valued Function holds (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g) proof let f1, f, g1, g be complex-valued Function; ::_thesis: (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g) A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_/_f)_+_(g1_/_g))_holds_ ((f1_/_f)_+_(g1_/_g))_._c_=_(((f1_(#)_g)_+_(g1_(#)_f))_/_(f_(#)_g))_._c let c be set ; ::_thesis: ( c in dom ((f1 / f) + (g1 / g)) implies ((f1 / f) + (g1 / g)) . c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) . c ) A2: dom (g ^) c= dom g by Th1; assume A3: c in dom ((f1 / f) + (g1 / g)) ; ::_thesis: ((f1 / f) + (g1 / g)) . c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) . c then A4: c in (dom (f1 / f)) /\ (dom (g1 / g)) by VALUED_1:def_1; then A5: c in dom (f1 / f) by XBOOLE_0:def_4; A6: c in dom (g1 / g) by A4, XBOOLE_0:def_4; A7: dom (f ^) c= dom f by Th1; A8: c in (dom (f1 (#) (f ^))) /\ (dom (g1 / g)) by A4, Th31; then c in dom (f1 (#) (f ^)) by XBOOLE_0:def_4; then A9: c in (dom f1) /\ (dom (f ^)) by VALUED_1:def_4; then A10: c in dom (f ^) by XBOOLE_0:def_4; then A11: f . c <> 0 by Th3; c in (dom (f1 (#) (f ^))) /\ (dom (g1 (#) (g ^))) by A8, Th31; then c in dom (g1 (#) (g ^)) by XBOOLE_0:def_4; then A12: c in (dom g1) /\ (dom (g ^)) by VALUED_1:def_4; then A13: c in dom (g ^) by XBOOLE_0:def_4; then A14: g . c <> 0 by Th3; c in dom g1 by A12, XBOOLE_0:def_4; then c in (dom g1) /\ (dom f) by A10, A7, XBOOLE_0:def_4; then A15: c in dom (g1 (#) f) by VALUED_1:def_4; c in dom f1 by A9, XBOOLE_0:def_4; then c in (dom f1) /\ (dom g) by A13, A2, XBOOLE_0:def_4; then c in dom (f1 (#) g) by VALUED_1:def_4; then c in (dom (f1 (#) g)) /\ (dom (g1 (#) f)) by A15, XBOOLE_0:def_4; then A16: c in dom ((f1 (#) g) + (g1 (#) f)) by VALUED_1:def_1; c in (dom (f ^)) /\ (dom (g ^)) by A10, A13, XBOOLE_0:def_4; then c in dom ((f ^) (#) (g ^)) by VALUED_1:def_4; then c in dom ((f (#) g) ^) by Th27; then c in (dom ((f1 (#) g) + (g1 (#) f))) /\ (dom ((f (#) g) ^)) by A16, XBOOLE_0:def_4; then c in dom (((f1 (#) g) + (g1 (#) f)) (#) ((f (#) g) ^)) by VALUED_1:def_4; then A17: c in dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) by Th31; thus ((f1 / f) + (g1 / g)) . c = ((f1 / f) . c) + ((g1 / g) . c) by A3, VALUED_1:def_1 .= ((f1 . c) * ((f . c) ")) + ((g1 / g) . c) by A5, Def1 .= ((f1 . c) * (1 * ((f . c) "))) + (((g1 . c) * 1) * ((g . c) ")) by A6, Def1 .= ((f1 . c) * (((g . c) * ((g . c) ")) * ((f . c) "))) + ((g1 . c) * (1 * ((g . c) "))) by A14, XCMPLX_0:def_7 .= ((f1 . c) * ((g . c) * (((g . c) ") * ((f . c) ")))) + ((g1 . c) * (((f . c) * ((f . c) ")) * ((g . c) "))) by A11, XCMPLX_0:def_7 .= ((f1 . c) * ((g . c) * (((g . c) * (f . c)) "))) + ((g1 . c) * ((f . c) * (((f . c) ") * ((g . c) ")))) by XCMPLX_1:204 .= ((f1 . c) * ((g . c) * (((f . c) * (g . c)) "))) + ((g1 . c) * ((f . c) * (((f . c) * (g . c)) "))) by XCMPLX_1:204 .= ((f1 . c) * ((g . c) * (((f (#) g) . c) "))) + ((g1 . c) * ((f . c) * (((f . c) * (g . c)) "))) by VALUED_1:5 .= (((f1 . c) * (g . c)) * (((f (#) g) . c) ")) + ((g1 . c) * ((f . c) * (((f (#) g) . c) "))) by VALUED_1:5 .= (((f1 (#) g) . c) * (((f (#) g) . c) ")) + (((g1 . c) * (f . c)) * (((f (#) g) . c) ")) by VALUED_1:5 .= (((f1 (#) g) . c) * (((f (#) g) . c) ")) + (((g1 (#) f) . c) * (((f (#) g) . c) ")) by VALUED_1:5 .= (((f1 (#) g) . c) + ((g1 (#) f) . c)) * (((f (#) g) . c) ") .= (((f1 (#) g) + (g1 (#) f)) . c) * (((f (#) g) . c) ") by A16, VALUED_1:def_1 .= (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) . c by A17, Def1 ; ::_thesis: verum end; dom ((f1 / f) + (g1 / g)) = (dom (f1 / f)) /\ (dom (g1 / g)) by VALUED_1:def_1 .= ((dom f1) /\ ((dom f) \ (f " {0}))) /\ (dom (g1 / g)) by Def1 .= ((dom f1) /\ ((dom f) \ (f " {0}))) /\ ((dom g1) /\ ((dom g) \ (g " {0}))) by Def1 .= ((dom f1) /\ ((dom f) /\ ((dom f) \ (f " {0})))) /\ ((dom g1) /\ ((dom g) \ (g " {0}))) by Th1 .= (((dom f) /\ ((dom f) \ (f " {0}))) /\ (dom f1)) /\ (((dom g) /\ ((dom g) \ (g " {0}))) /\ (dom g1)) by Th1 .= ((dom f) /\ ((dom f) \ (f " {0}))) /\ ((dom f1) /\ (((dom g) /\ ((dom g) \ (g " {0}))) /\ (dom g1))) by XBOOLE_1:16 .= ((dom f) /\ ((dom f) \ (f " {0}))) /\ (((dom f1) /\ ((dom g) /\ ((dom g) \ (g " {0})))) /\ (dom g1)) by XBOOLE_1:16 .= ((dom f) /\ ((dom f) \ (f " {0}))) /\ ((((dom f1) /\ (dom g)) /\ ((dom g) \ (g " {0}))) /\ (dom g1)) by XBOOLE_1:16 .= ((dom f) /\ ((dom f) \ (f " {0}))) /\ (((dom (f1 (#) g)) /\ ((dom g) \ (g " {0}))) /\ (dom g1)) by VALUED_1:def_4 .= ((dom f) /\ ((dom f) \ (f " {0}))) /\ ((dom (f1 (#) g)) /\ ((dom g1) /\ ((dom g) \ (g " {0})))) by XBOOLE_1:16 .= (dom (f1 (#) g)) /\ ((((dom f) \ (f " {0})) /\ (dom f)) /\ ((dom g1) /\ ((dom g) \ (g " {0})))) by XBOOLE_1:16 .= (dom (f1 (#) g)) /\ (((dom f) \ (f " {0})) /\ ((dom f) /\ ((dom g1) /\ ((dom g) \ (g " {0}))))) by XBOOLE_1:16 .= (dom (f1 (#) g)) /\ (((dom f) \ (f " {0})) /\ (((dom g1) /\ (dom f)) /\ ((dom g) \ (g " {0})))) by XBOOLE_1:16 .= (dom (f1 (#) g)) /\ (((dom f) \ (f " {0})) /\ ((dom (g1 (#) f)) /\ ((dom g) \ (g " {0})))) by VALUED_1:def_4 .= (dom (f1 (#) g)) /\ ((dom (g1 (#) f)) /\ (((dom f) \ (f " {0})) /\ ((dom g) \ (g " {0})))) by XBOOLE_1:16 .= ((dom (f1 (#) g)) /\ (dom (g1 (#) f))) /\ (((dom f) \ (f " {0})) /\ ((dom g) \ (g " {0}))) by XBOOLE_1:16 .= (dom ((f1 (#) g) + (g1 (#) f))) /\ (((dom f) \ (f " {0})) /\ ((dom g) \ (g " {0}))) by VALUED_1:def_1 .= (dom ((f1 (#) g) + (g1 (#) f))) /\ ((dom (f (#) g)) \ ((f (#) g) " {0})) by Th2 .= dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) by Def1 ; hence (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g) by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: RFUNCT_1:41 for f, g, f1, g1 being complex-valued Function holds (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1) proof let f, g, f1, g1 be complex-valued Function; ::_thesis: (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1) thus (f / g) / (f1 / g1) = (f / g) (#) ((f1 / g1) ^) by Th31 .= (f / g) (#) ((g1 | (dom (g1 ^))) / f1) by Th35 .= (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1) by Th34 ; ::_thesis: verum end; theorem :: RFUNCT_1:42 for f1, f, g1, g being complex-valued Function holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g) proof let f1, f, g1, g be complex-valued Function; ::_thesis: (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g) thus (f1 / f) - (g1 / g) = (f1 / f) + (((- 1) (#) g1) / g) by Th32 .= ((f1 (#) g) + (((- 1) (#) g1) (#) f)) / (f (#) g) by Th40 .= ((f1 (#) g) - (g1 (#) f)) / (f (#) g) by Th12 ; ::_thesis: verum end; theorem :: RFUNCT_1:43 for f1, f2 being complex-valued Function holds abs (f1 / f2) = (abs f1) / (abs f2) proof let f1, f2 be complex-valued Function; ::_thesis: abs (f1 / f2) = (abs f1) / (abs f2) thus abs (f1 / f2) = abs (f1 (#) (f2 ^)) by Th31 .= (abs f1) (#) (abs (f2 ^)) by Th24 .= (abs f1) (#) ((abs f2) ^) by Th30 .= (abs f1) / (abs f2) by Th31 ; ::_thesis: verum end; theorem Th44: :: RFUNCT_1:44 for X being set for f1, f2 being complex-valued Function holds ( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) ) proof let X be set ; ::_thesis: for f1, f2 being complex-valued Function holds ( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) ) let f1, f2 be complex-valued Function; ::_thesis: ( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) ) A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_+_f2)_|_X)_holds_ ((f1_+_f2)_|_X)_._c_=_((f1_|_X)_+_(f2_|_X))_._c let c be set ; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) . c = ((f1 | X) + (f2 | X)) . c ) assume A2: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) . c = ((f1 | X) + (f2 | X)) . c then A3: c in (dom (f1 + f2)) /\ X by RELAT_1:61; then A4: c in X by XBOOLE_0:def_4; A5: c in dom (f1 + f2) by A3, XBOOLE_0:def_4; then A6: c in (dom f1) /\ (dom f2) by VALUED_1:def_1; then c in dom f2 by XBOOLE_0:def_4; then c in (dom f2) /\ X by A4, XBOOLE_0:def_4; then A7: c in dom (f2 | X) by RELAT_1:61; c in dom f1 by A6, XBOOLE_0:def_4; then c in (dom f1) /\ X by A4, XBOOLE_0:def_4; then A8: c in dom (f1 | X) by RELAT_1:61; then c in (dom (f1 | X)) /\ (dom (f2 | X)) by A7, XBOOLE_0:def_4; then A9: c in dom ((f1 | X) + (f2 | X)) by VALUED_1:def_1; thus ((f1 + f2) | X) . c = (f1 + f2) . c by A2, FUNCT_1:47 .= (f1 . c) + (f2 . c) by A5, VALUED_1:def_1 .= ((f1 | X) . c) + (f2 . c) by A8, FUNCT_1:47 .= ((f1 | X) . c) + ((f2 | X) . c) by A7, FUNCT_1:47 .= ((f1 | X) + (f2 | X)) . c by A9, VALUED_1:def_1 ; ::_thesis: verum end; dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ (X /\ X) by VALUED_1:def_1 .= (dom f1) /\ ((dom f2) /\ (X /\ X)) by XBOOLE_1:16 .= (dom f1) /\ (((dom f2) /\ X) /\ X) by XBOOLE_1:16 .= (dom f1) /\ (X /\ (dom (f2 | X))) by RELAT_1:61 .= ((dom f1) /\ X) /\ (dom (f2 | X)) by XBOOLE_1:16 .= (dom (f1 | X)) /\ (dom (f2 | X)) by RELAT_1:61 .= dom ((f1 | X) + (f2 | X)) by VALUED_1:def_1 ; hence (f1 + f2) | X = (f1 | X) + (f2 | X) by A1, FUNCT_1:2; ::_thesis: ( (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) ) A10: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_+_f2)_|_X)_holds_ ((f1_+_f2)_|_X)_._c_=_((f1_|_X)_+_f2)_._c let c be set ; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) . c = ((f1 | X) + f2) . c ) assume A11: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) . c = ((f1 | X) + f2) . c then A12: c in (dom (f1 + f2)) /\ X by RELAT_1:61; then A13: c in X by XBOOLE_0:def_4; A14: c in dom (f1 + f2) by A12, XBOOLE_0:def_4; then A15: c in (dom f1) /\ (dom f2) by VALUED_1:def_1; then c in dom f1 by XBOOLE_0:def_4; then c in (dom f1) /\ X by A13, XBOOLE_0:def_4; then A16: c in dom (f1 | X) by RELAT_1:61; c in dom f2 by A15, XBOOLE_0:def_4; then c in (dom (f1 | X)) /\ (dom f2) by A16, XBOOLE_0:def_4; then A17: c in dom ((f1 | X) + f2) by VALUED_1:def_1; thus ((f1 + f2) | X) . c = (f1 + f2) . c by A11, FUNCT_1:47 .= (f1 . c) + (f2 . c) by A14, VALUED_1:def_1 .= ((f1 | X) . c) + (f2 . c) by A16, FUNCT_1:47 .= ((f1 | X) + f2) . c by A17, VALUED_1:def_1 ; ::_thesis: verum end; dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ X by VALUED_1:def_1 .= ((dom f1) /\ X) /\ (dom f2) by XBOOLE_1:16 .= (dom (f1 | X)) /\ (dom f2) by RELAT_1:61 .= dom ((f1 | X) + f2) by VALUED_1:def_1 ; hence (f1 + f2) | X = (f1 | X) + f2 by A10, FUNCT_1:2; ::_thesis: (f1 + f2) | X = f1 + (f2 | X) A18: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_+_f2)_|_X)_holds_ ((f1_+_f2)_|_X)_._c_=_(f1_+_(f2_|_X))_._c let c be set ; ::_thesis: ( c in dom ((f1 + f2) | X) implies ((f1 + f2) | X) . c = (f1 + (f2 | X)) . c ) assume A19: c in dom ((f1 + f2) | X) ; ::_thesis: ((f1 + f2) | X) . c = (f1 + (f2 | X)) . c then A20: c in (dom (f1 + f2)) /\ X by RELAT_1:61; then A21: c in X by XBOOLE_0:def_4; A22: c in dom (f1 + f2) by A20, XBOOLE_0:def_4; then A23: c in (dom f1) /\ (dom f2) by VALUED_1:def_1; then c in dom f2 by XBOOLE_0:def_4; then c in (dom f2) /\ X by A21, XBOOLE_0:def_4; then A24: c in dom (f2 | X) by RELAT_1:61; c in dom f1 by A23, XBOOLE_0:def_4; then c in (dom f1) /\ (dom (f2 | X)) by A24, XBOOLE_0:def_4; then A25: c in dom (f1 + (f2 | X)) by VALUED_1:def_1; thus ((f1 + f2) | X) . c = (f1 + f2) . c by A19, FUNCT_1:47 .= (f1 . c) + (f2 . c) by A22, VALUED_1:def_1 .= (f1 . c) + ((f2 | X) . c) by A24, FUNCT_1:47 .= (f1 + (f2 | X)) . c by A25, VALUED_1:def_1 ; ::_thesis: verum end; dom ((f1 + f2) | X) = (dom (f1 + f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ X by VALUED_1:def_1 .= (dom f1) /\ ((dom f2) /\ X) by XBOOLE_1:16 .= (dom f1) /\ (dom (f2 | X)) by RELAT_1:61 .= dom (f1 + (f2 | X)) by VALUED_1:def_1 ; hence (f1 + f2) | X = f1 + (f2 | X) by A18, FUNCT_1:2; ::_thesis: verum end; theorem Th45: :: RFUNCT_1:45 for X being set for f1, f2 being complex-valued Function holds ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) ) proof let X be set ; ::_thesis: for f1, f2 being complex-valued Function holds ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) ) let f1, f2 be complex-valued Function; ::_thesis: ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) ) A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_ ((f1_(#)_f2)_|_X)_._c_=_((f1_|_X)_(#)_(f2_|_X))_._c let c be set ; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) . c = ((f1 | X) (#) (f2 | X)) . c ) assume A2: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) . c = ((f1 | X) (#) (f2 | X)) . c then A3: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61; then A4: c in X by XBOOLE_0:def_4; c in dom (f1 (#) f2) by A3, XBOOLE_0:def_4; then A5: c in (dom f1) /\ (dom f2) by VALUED_1:def_4; then c in dom f1 by XBOOLE_0:def_4; then c in (dom f1) /\ X by A4, XBOOLE_0:def_4; then A6: c in dom (f1 | X) by RELAT_1:61; c in dom f2 by A5, XBOOLE_0:def_4; then c in (dom f2) /\ X by A4, XBOOLE_0:def_4; then A7: c in dom (f2 | X) by RELAT_1:61; thus ((f1 (#) f2) | X) . c = (f1 (#) f2) . c by A2, FUNCT_1:47 .= (f1 . c) * (f2 . c) by VALUED_1:5 .= ((f1 | X) . c) * (f2 . c) by A6, FUNCT_1:47 .= ((f1 | X) . c) * ((f2 | X) . c) by A7, FUNCT_1:47 .= ((f1 | X) (#) (f2 | X)) . c by VALUED_1:5 ; ::_thesis: verum end; dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ (X /\ X) by VALUED_1:def_4 .= (dom f1) /\ ((dom f2) /\ (X /\ X)) by XBOOLE_1:16 .= (dom f1) /\ (((dom f2) /\ X) /\ X) by XBOOLE_1:16 .= (dom f1) /\ (X /\ (dom (f2 | X))) by RELAT_1:61 .= ((dom f1) /\ X) /\ (dom (f2 | X)) by XBOOLE_1:16 .= (dom (f1 | X)) /\ (dom (f2 | X)) by RELAT_1:61 .= dom ((f1 | X) (#) (f2 | X)) by VALUED_1:def_4 ; hence (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) by A1, FUNCT_1:2; ::_thesis: ( (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) ) A8: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_ ((f1_(#)_f2)_|_X)_._c_=_((f1_|_X)_(#)_f2)_._c let c be set ; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) . c = ((f1 | X) (#) f2) . c ) assume A9: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) . c = ((f1 | X) (#) f2) . c then A10: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61; then c in dom (f1 (#) f2) by XBOOLE_0:def_4; then c in (dom f1) /\ (dom f2) by VALUED_1:def_4; then A11: c in dom f1 by XBOOLE_0:def_4; c in X by A10, XBOOLE_0:def_4; then c in (dom f1) /\ X by A11, XBOOLE_0:def_4; then A12: c in dom (f1 | X) by RELAT_1:61; thus ((f1 (#) f2) | X) . c = (f1 (#) f2) . c by A9, FUNCT_1:47 .= (f1 . c) * (f2 . c) by VALUED_1:5 .= ((f1 | X) . c) * (f2 . c) by A12, FUNCT_1:47 .= ((f1 | X) (#) f2) . c by VALUED_1:5 ; ::_thesis: verum end; dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ X by VALUED_1:def_4 .= ((dom f1) /\ X) /\ (dom f2) by XBOOLE_1:16 .= (dom (f1 | X)) /\ (dom f2) by RELAT_1:61 .= dom ((f1 | X) (#) f2) by VALUED_1:def_4 ; hence (f1 (#) f2) | X = (f1 | X) (#) f2 by A8, FUNCT_1:2; ::_thesis: (f1 (#) f2) | X = f1 (#) (f2 | X) A13: now__::_thesis:_for_c_being_set_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_ ((f1_(#)_f2)_|_X)_._c_=_(f1_(#)_(f2_|_X))_._c let c be set ; ::_thesis: ( c in dom ((f1 (#) f2) | X) implies ((f1 (#) f2) | X) . c = (f1 (#) (f2 | X)) . c ) assume A14: c in dom ((f1 (#) f2) | X) ; ::_thesis: ((f1 (#) f2) | X) . c = (f1 (#) (f2 | X)) . c then A15: c in (dom (f1 (#) f2)) /\ X by RELAT_1:61; then c in dom (f1 (#) f2) by XBOOLE_0:def_4; then c in (dom f1) /\ (dom f2) by VALUED_1:def_4; then A16: c in dom f2 by XBOOLE_0:def_4; c in X by A15, XBOOLE_0:def_4; then c in (dom f2) /\ X by A16, XBOOLE_0:def_4; then A17: c in dom (f2 | X) by RELAT_1:61; thus ((f1 (#) f2) | X) . c = (f1 (#) f2) . c by A14, FUNCT_1:47 .= (f1 . c) * (f2 . c) by VALUED_1:5 .= (f1 . c) * ((f2 | X) . c) by A17, FUNCT_1:47 .= (f1 (#) (f2 | X)) . c by VALUED_1:5 ; ::_thesis: verum end; dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ X by VALUED_1:def_4 .= (dom f1) /\ ((dom f2) /\ X) by XBOOLE_1:16 .= (dom f1) /\ (dom (f2 | X)) by RELAT_1:61 .= dom (f1 (#) (f2 | X)) by VALUED_1:def_4 ; hence (f1 (#) f2) | X = f1 (#) (f2 | X) by A13, FUNCT_1:2; ::_thesis: verum end; theorem Th46: :: RFUNCT_1:46 for X being set for f being complex-valued Function holds ( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & (abs f) | X = abs (f | X) ) proof let X be set ; ::_thesis: for f being complex-valued Function holds ( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & (abs f) | X = abs (f | X) ) let f be complex-valued Function; ::_thesis: ( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & (abs f) | X = abs (f | X) ) A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((-_f)_|_X)_holds_ ((-_f)_|_X)_._c_=_(-_(f_|_X))_._c let c be set ; ::_thesis: ( c in dom ((- f) | X) implies ((- f) | X) . c = (- (f | X)) . c ) assume A2: c in dom ((- f) | X) ; ::_thesis: ((- f) | X) . c = (- (f | X)) . c then A3: c in (dom (- f)) /\ X by RELAT_1:61; then c in dom (- f) by XBOOLE_0:def_4; then A4: c in dom f by VALUED_1:8; c in X by A3, XBOOLE_0:def_4; then c in (dom f) /\ X by A4, XBOOLE_0:def_4; then A5: c in dom (f | X) by RELAT_1:61; thus ((- f) | X) . c = (- f) . c by A2, FUNCT_1:47 .= - (f . c) by VALUED_1:8 .= - ((f | X) . c) by A5, FUNCT_1:47 .= (- (f | X)) . c by VALUED_1:8 ; ::_thesis: verum end; dom ((- f) | X) = (dom (- f)) /\ X by RELAT_1:61 .= (dom f) /\ X by VALUED_1:8 .= dom (f | X) by RELAT_1:61 .= dom (- (f | X)) by VALUED_1:8 ; hence (- f) | X = - (f | X) by A1, FUNCT_1:2; ::_thesis: ( (f ^) | X = (f | X) ^ & (abs f) | X = abs (f | X) ) A6: dom ((f ^) | X) = (dom (f ^)) /\ X by RELAT_1:61 .= ((dom f) \ (f " {0})) /\ X by Def2 .= ((dom f) /\ X) \ ((f " {0}) /\ X) by XBOOLE_1:50 .= (dom (f | X)) \ (X /\ (f " {0})) by RELAT_1:61 .= (dom (f | X)) \ ((f | X) " {0}) by FUNCT_1:70 .= dom ((f | X) ^) by Def2 ; A7: dom ((f | X) ^) c= dom (f | X) by Th1; now__::_thesis:_for_c_being_set_st_c_in_dom_((f_^)_|_X)_holds_ ((f_^)_|_X)_._c_=_((f_|_X)_^)_._c let c be set ; ::_thesis: ( c in dom ((f ^) | X) implies ((f ^) | X) . c = ((f | X) ^) . c ) assume A8: c in dom ((f ^) | X) ; ::_thesis: ((f ^) | X) . c = ((f | X) ^) . c then c in (dom (f ^)) /\ X by RELAT_1:61; then A9: c in dom (f ^) by XBOOLE_0:def_4; thus ((f ^) | X) . c = (f ^) . c by A8, FUNCT_1:47 .= (f . c) " by A9, Def2 .= ((f | X) . c) " by A7, A6, A8, FUNCT_1:47 .= ((f | X) ^) . c by A6, A8, Def2 ; ::_thesis: verum end; hence (f ^) | X = (f | X) ^ by A6, FUNCT_1:2; ::_thesis: (abs f) | X = abs (f | X) A10: dom ((abs f) | X) = (dom (abs f)) /\ X by RELAT_1:61 .= (dom f) /\ X by VALUED_1:def_11 .= dom (f | X) by RELAT_1:61 .= dom (abs (f | X)) by VALUED_1:def_11 ; now__::_thesis:_for_c_being_set_st_c_in_dom_((abs_f)_|_X)_holds_ ((abs_f)_|_X)_._c_=_(abs_(f_|_X))_._c let c be set ; ::_thesis: ( c in dom ((abs f) | X) implies ((abs f) | X) . c = (abs (f | X)) . c ) assume A11: c in dom ((abs f) | X) ; ::_thesis: ((abs f) | X) . c = (abs (f | X)) . c then A12: c in dom (f | X) by A10, VALUED_1:def_11; thus ((abs f) | X) . c = (abs f) . c by A11, FUNCT_1:47 .= abs (f . c) by VALUED_1:18 .= abs ((f | X) . c) by A12, FUNCT_1:47 .= (abs (f | X)) . c by VALUED_1:18 ; ::_thesis: verum end; hence (abs f) | X = abs (f | X) by A10, FUNCT_1:2; ::_thesis: verum end; theorem :: RFUNCT_1:47 for X being set for f1, f2 being complex-valued Function holds ( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) ) proof let X be set ; ::_thesis: for f1, f2 being complex-valued Function holds ( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) ) let f1, f2 be complex-valued Function; ::_thesis: ( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) ) thus (f1 - f2) | X = (f1 | X) + ((- f2) | X) by Th44 .= (f1 | X) - (f2 | X) by Th46 ; ::_thesis: ( (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) ) thus (f1 - f2) | X = (f1 | X) - f2 by Th44; ::_thesis: (f1 - f2) | X = f1 - (f2 | X) thus (f1 - f2) | X = f1 + ((- f2) | X) by Th44 .= f1 - (f2 | X) by Th46 ; ::_thesis: verum end; theorem :: RFUNCT_1:48 for X being set for f1, f2 being complex-valued Function holds ( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) ) proof let X be set ; ::_thesis: for f1, f2 being complex-valued Function holds ( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) ) let f1, f2 be complex-valued Function; ::_thesis: ( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) ) thus (f1 / f2) | X = (f1 (#) (f2 ^)) | X by Th31 .= (f1 | X) (#) ((f2 ^) | X) by Th45 .= (f1 | X) (#) ((f2 | X) ^) by Th46 .= (f1 | X) / (f2 | X) by Th31 ; ::_thesis: ( (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) ) thus (f1 / f2) | X = (f1 (#) (f2 ^)) | X by Th31 .= (f1 | X) (#) (f2 ^) by Th45 .= (f1 | X) / f2 by Th31 ; ::_thesis: (f1 / f2) | X = f1 / (f2 | X) thus (f1 / f2) | X = (f1 (#) (f2 ^)) | X by Th31 .= f1 (#) ((f2 ^) | X) by Th45 .= f1 (#) ((f2 | X) ^) by Th46 .= f1 / (f2 | X) by Th31 ; ::_thesis: verum end; theorem Th49: :: RFUNCT_1:49 for X being set for f being complex-valued Function for r being complex number holds (r (#) f) | X = r (#) (f | X) proof let X be set ; ::_thesis: for f being complex-valued Function for r being complex number holds (r (#) f) | X = r (#) (f | X) let f be complex-valued Function; ::_thesis: for r being complex number holds (r (#) f) | X = r (#) (f | X) let r be complex number ; ::_thesis: (r (#) f) | X = r (#) (f | X) A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((r_(#)_f)_|_X)_holds_ ((r_(#)_f)_|_X)_._c_=_(r_(#)_(f_|_X))_._c let c be set ; ::_thesis: ( c in dom ((r (#) f) | X) implies ((r (#) f) | X) . c = (r (#) (f | X)) . c ) assume A2: c in dom ((r (#) f) | X) ; ::_thesis: ((r (#) f) | X) . c = (r (#) (f | X)) . c then A3: c in (dom (r (#) f)) /\ X by RELAT_1:61; then A4: c in X by XBOOLE_0:def_4; A5: c in dom (r (#) f) by A3, XBOOLE_0:def_4; then c in dom f by VALUED_1:def_5; then c in (dom f) /\ X by A4, XBOOLE_0:def_4; then A6: c in dom (f | X) by RELAT_1:61; then A7: c in dom (r (#) (f | X)) by VALUED_1:def_5; thus ((r (#) f) | X) . c = (r (#) f) . c by A2, FUNCT_1:47 .= r * (f . c) by A5, VALUED_1:def_5 .= r * ((f | X) . c) by A6, FUNCT_1:47 .= (r (#) (f | X)) . c by A7, VALUED_1:def_5 ; ::_thesis: verum end; dom ((r (#) f) | X) = (dom (r (#) f)) /\ X by RELAT_1:61 .= (dom f) /\ X by VALUED_1:def_5 .= dom (f | X) by RELAT_1:61 .= dom (r (#) (f | X)) by VALUED_1:def_5 ; hence (r (#) f) | X = r (#) (f | X) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th50: :: RFUNCT_1:50 for C being non empty set for f1, f2 being PartFunc of C,REAL holds ( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) ) proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,REAL holds ( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) ) let f1, f2 be PartFunc of C,REAL; ::_thesis: ( ( f1 is total & f2 is total implies f1 + f2 is total ) & ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) ) thus ( ( f1 is total & f2 is total ) iff f1 + f2 is total ) ::_thesis: ( ( f1 is total & f2 is total implies f1 - f2 is total ) & ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) & ( f1 is total & f2 is total implies f1 (#) f2 is total ) & ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) ) proof thus ( f1 is total & f2 is total implies f1 + f2 is total ) ; ::_thesis: ( f1 + f2 is total implies ( f1 is total & f2 is total ) ) assume f1 + f2 is total ; ::_thesis: ( f1 is total & f2 is total ) then dom (f1 + f2) = C by PARTFUN1:def_2; then A4: (dom f1) /\ (dom f2) = C by VALUED_1:def_1; then A5: C c= dom f2 by XBOOLE_1:17; C c= dom f1 by A4, XBOOLE_1:17; hence ( dom f1 = C & dom f2 = C ) by A5, XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum end; thus ( ( f1 is total & f2 is total ) iff f1 - f2 is total ) ::_thesis: ( ( f1 is total & f2 is total ) iff f1 (#) f2 is total ) proof thus ( f1 is total & f2 is total implies f1 - f2 is total ) ; ::_thesis: ( f1 - f2 is total implies ( f1 is total & f2 is total ) ) assume f1 - f2 is total ; ::_thesis: ( f1 is total & f2 is total ) then dom (f1 - f2) = C by PARTFUN1:def_2; then A9: (dom f1) /\ (dom f2) = C by VALUED_1:12; then A10: C c= dom f2 by XBOOLE_1:17; C c= dom f1 by A9, XBOOLE_1:17; hence ( dom f1 = C & dom f2 = C ) by A10, XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum end; thus ( f1 is total & f2 is total implies f1 (#) f2 is total ) ; ::_thesis: ( f1 (#) f2 is total implies ( f1 is total & f2 is total ) ) assume f1 (#) f2 is total ; ::_thesis: ( f1 is total & f2 is total ) then dom (f1 (#) f2) = C by PARTFUN1:def_2; then A14: (dom f1) /\ (dom f2) = C by VALUED_1:def_4; then A15: C c= dom f2 by XBOOLE_1:17; C c= dom f1 by A14, XBOOLE_1:17; hence ( dom f1 = C & dom f2 = C ) by A15, XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum end; theorem Th51: :: RFUNCT_1:51 for C being non empty set for r being real number for f being PartFunc of C,REAL holds ( f is total iff r (#) f is total ) proof let C be non empty set ; ::_thesis: for r being real number for f being PartFunc of C,REAL holds ( f is total iff r (#) f is total ) let r be real number ; ::_thesis: for f being PartFunc of C,REAL holds ( f is total iff r (#) f is total ) let f be PartFunc of C,REAL; ::_thesis: ( f is total iff r (#) f is total ) thus ( f is total implies r (#) f is total ) ; ::_thesis: ( r (#) f is total implies f is total ) assume r (#) f is total ; ::_thesis: f is total then dom (r (#) f) = C by PARTFUN1:def_2; hence dom f = C by VALUED_1:def_5; :: according to PARTFUN1:def_2 ::_thesis: verum end; theorem :: RFUNCT_1:52 for C being non empty set for f being PartFunc of C,REAL holds ( f is total iff - f is total ) by Th51; theorem :: RFUNCT_1:53 for C being non empty set for f being PartFunc of C,REAL holds ( f is total iff abs f is total ) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,REAL holds ( f is total iff abs f is total ) let f be PartFunc of C,REAL; ::_thesis: ( f is total iff abs f is total ) thus ( f is total implies abs f is total ) ; ::_thesis: ( abs f is total implies f is total ) assume abs f is total ; ::_thesis: f is total then dom (abs f) = C by PARTFUN1:def_2; hence dom f = C by VALUED_1:def_11; :: according to PARTFUN1:def_2 ::_thesis: verum end; theorem Th54: :: RFUNCT_1:54 for C being non empty set for f being PartFunc of C,REAL holds ( f ^ is total iff ( f " {0} = {} & f is total ) ) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,REAL holds ( f ^ is total iff ( f " {0} = {} & f is total ) ) let f be PartFunc of C,REAL; ::_thesis: ( f ^ is total iff ( f " {0} = {} & f is total ) ) thus ( f ^ is total implies ( f " {0} = {} & f is total ) ) ::_thesis: ( f " {0} = {} & f is total implies f ^ is total ) proof assume f ^ is total ; ::_thesis: ( f " {0} = {} & f is total ) then A1: dom (f ^) = C by PARTFUN1:def_2; f " {0} c= C ; then f " {0} c= (dom f) \ (f " {0}) by A1, Def2; hence f " {0} = {} by XBOOLE_1:38; ::_thesis: f is total then C = (dom f) \ {} by A1, Def2; hence dom f = C ; :: according to PARTFUN1:def_2 ::_thesis: verum end; assume that A2: f " {0} = {} and A3: f is total ; ::_thesis: f ^ is total thus dom (f ^) = (dom f) \ (f " {0}) by Def2 .= C by A2, A3, PARTFUN1:def_2 ; :: according to PARTFUN1:def_2 ::_thesis: verum end; theorem Th55: :: RFUNCT_1:55 for C being non empty set for f1, f2 being PartFunc of C,REAL holds ( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total ) proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,REAL holds ( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total ) let f1, f2 be PartFunc of C,REAL; ::_thesis: ( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total ) thus ( f1 is total & f2 " {0} = {} & f2 is total implies f1 / f2 is total ) ::_thesis: ( f1 / f2 is total implies ( f1 is total & f2 " {0} = {} & f2 is total ) ) proof assume that A1: f1 is total and A2: f2 " {0} = {} and A3: f2 is total ; ::_thesis: f1 / f2 is total f2 ^ is total by A2, A3, Th54; then f1 (#) (f2 ^) is total by A1; hence f1 / f2 is total by Th31; ::_thesis: verum end; assume f1 / f2 is total ; ::_thesis: ( f1 is total & f2 " {0} = {} & f2 is total ) then A4: f1 (#) (f2 ^) is total by Th31; hence f1 is total by Th50; ::_thesis: ( f2 " {0} = {} & f2 is total ) f2 ^ is total by A4, Th50; hence ( f2 " {0} = {} & f2 is total ) by Th54; ::_thesis: verum end; theorem :: RFUNCT_1:56 for C being non empty set for c being Element of C for f1, f2 being PartFunc of C,REAL st f1 is total & f2 is total holds ( (f1 + f2) . c = (f1 . c) + (f2 . c) & (f1 - f2) . c = (f1 . c) - (f2 . c) & (f1 (#) f2) . c = (f1 . c) * (f2 . c) ) proof let C be non empty set ; ::_thesis: for c being Element of C for f1, f2 being PartFunc of C,REAL st f1 is total & f2 is total holds ( (f1 + f2) . c = (f1 . c) + (f2 . c) & (f1 - f2) . c = (f1 . c) - (f2 . c) & (f1 (#) f2) . c = (f1 . c) * (f2 . c) ) let c be Element of C; ::_thesis: for f1, f2 being PartFunc of C,REAL st f1 is total & f2 is total holds ( (f1 + f2) . c = (f1 . c) + (f2 . c) & (f1 - f2) . c = (f1 . c) - (f2 . c) & (f1 (#) f2) . c = (f1 . c) * (f2 . c) ) let f1, f2 be PartFunc of C,REAL; ::_thesis: ( f1 is total & f2 is total implies ( (f1 + f2) . c = (f1 . c) + (f2 . c) & (f1 - f2) . c = (f1 . c) - (f2 . c) & (f1 (#) f2) . c = (f1 . c) * (f2 . c) ) ) assume that A1: f1 is total and A2: f2 is total ; ::_thesis: ( (f1 + f2) . c = (f1 . c) + (f2 . c) & (f1 - f2) . c = (f1 . c) - (f2 . c) & (f1 (#) f2) . c = (f1 . c) * (f2 . c) ) f1 + f2 is total by A1, A2; then dom (f1 + f2) = C by PARTFUN1:def_2; hence (f1 + f2) . c = (f1 . c) + (f2 . c) by VALUED_1:def_1; ::_thesis: ( (f1 - f2) . c = (f1 . c) - (f2 . c) & (f1 (#) f2) . c = (f1 . c) * (f2 . c) ) f1 - f2 is total by A1, A2; then dom (f1 - f2) = C by PARTFUN1:def_2; hence (f1 - f2) . c = (f1 . c) - (f2 . c) by VALUED_1:13; ::_thesis: (f1 (#) f2) . c = (f1 . c) * (f2 . c) thus (f1 (#) f2) . c = (f1 . c) * (f2 . c) by VALUED_1:5; ::_thesis: verum end; theorem :: RFUNCT_1:57 for C being non empty set for c being Element of C for r being real number for f being PartFunc of C,REAL st f is total holds (r (#) f) . c = r * (f . c) proof let C be non empty set ; ::_thesis: for c being Element of C for r being real number for f being PartFunc of C,REAL st f is total holds (r (#) f) . c = r * (f . c) let c be Element of C; ::_thesis: for r being real number for f being PartFunc of C,REAL st f is total holds (r (#) f) . c = r * (f . c) let r be real number ; ::_thesis: for f being PartFunc of C,REAL st f is total holds (r (#) f) . c = r * (f . c) let f be PartFunc of C,REAL; ::_thesis: ( f is total implies (r (#) f) . c = r * (f . c) ) assume f is total ; ::_thesis: (r (#) f) . c = r * (f . c) then r (#) f is total ; then dom (r (#) f) = C by PARTFUN1:def_2; hence (r (#) f) . c = r * (f . c) by VALUED_1:def_5; ::_thesis: verum end; theorem :: RFUNCT_1:58 for C being non empty set for c being Element of C for f being PartFunc of C,REAL st f is total holds ( (- f) . c = - (f . c) & (abs f) . c = abs (f . c) ) by VALUED_1:8, VALUED_1:18; theorem :: RFUNCT_1:59 for C being non empty set for c being Element of C for f being PartFunc of C,REAL st f ^ is total holds (f ^) . c = (f . c) " proof let C be non empty set ; ::_thesis: for c being Element of C for f being PartFunc of C,REAL st f ^ is total holds (f ^) . c = (f . c) " let c be Element of C; ::_thesis: for f being PartFunc of C,REAL st f ^ is total holds (f ^) . c = (f . c) " let f be PartFunc of C,REAL; ::_thesis: ( f ^ is total implies (f ^) . c = (f . c) " ) assume f ^ is total ; ::_thesis: (f ^) . c = (f . c) " then dom (f ^) = C by PARTFUN1:def_2; hence (f ^) . c = (f . c) " by Def2; ::_thesis: verum end; theorem :: RFUNCT_1:60 for C being non empty set for c being Element of C for f1, f2 being PartFunc of C,REAL st f1 is total & f2 ^ is total holds (f1 / f2) . c = (f1 . c) * ((f2 . c) ") proof let C be non empty set ; ::_thesis: for c being Element of C for f1, f2 being PartFunc of C,REAL st f1 is total & f2 ^ is total holds (f1 / f2) . c = (f1 . c) * ((f2 . c) ") let c be Element of C; ::_thesis: for f1, f2 being PartFunc of C,REAL st f1 is total & f2 ^ is total holds (f1 / f2) . c = (f1 . c) * ((f2 . c) ") let f1, f2 be PartFunc of C,REAL; ::_thesis: ( f1 is total & f2 ^ is total implies (f1 / f2) . c = (f1 . c) * ((f2 . c) ") ) assume that A1: f1 is total and A2: f2 ^ is total ; ::_thesis: (f1 / f2) . c = (f1 . c) * ((f2 . c) ") A3: f2 is total by A2, Th54; f2 " {0} = {} by A2, Th54; then f1 / f2 is total by A1, A3, Th55; then dom (f1 / f2) = C by PARTFUN1:def_2; hence (f1 / f2) . c = (f1 . c) * ((f2 . c) ") by Def1; ::_thesis: verum end; definition let X, C be set ; :: original: chi redefine func chi (X,C) -> PartFunc of C,REAL; coherence chi (X,C) is PartFunc of C,REAL proof now__::_thesis:_for_x_being_set_st_x_in_rng_(chi_(X,C))_holds_ x_in_REAL let x be set ; ::_thesis: ( x in rng (chi (X,C)) implies x in REAL ) assume x in rng (chi (X,C)) ; ::_thesis: x in REAL then ( x = 0 or x = 1 ) by TARSKI:def_2; hence x in REAL ; ::_thesis: verum end; then A1: rng (chi (X,C)) c= REAL by TARSKI:def_3; dom (chi (X,C)) = C by FUNCT_3:def_3; hence chi (X,C) is PartFunc of C,REAL by A1, RELSET_1:4; ::_thesis: verum end; end; registration let X, C be set ; cluster chi (X,C) -> total for PartFunc of C,REAL; coherence for b1 being PartFunc of C,REAL st b1 = chi (X,C) holds b1 is total proof dom (chi (X,C)) = C by FUNCT_3:def_3; hence for b1 being PartFunc of C,REAL st b1 = chi (X,C) holds b1 is total by PARTFUN1:def_2; ::_thesis: verum end; end; theorem Th61: :: RFUNCT_1:61 for X being set for C being non empty set for f being PartFunc of C,REAL holds ( f = chi (X,C) iff ( dom f = C & ( for c being Element of C holds ( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) ) proof let X be set ; ::_thesis: for C being non empty set for f being PartFunc of C,REAL holds ( f = chi (X,C) iff ( dom f = C & ( for c being Element of C holds ( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) ) let C be non empty set ; ::_thesis: for f being PartFunc of C,REAL holds ( f = chi (X,C) iff ( dom f = C & ( for c being Element of C holds ( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) ) let f be PartFunc of C,REAL; ::_thesis: ( f = chi (X,C) iff ( dom f = C & ( for c being Element of C holds ( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) ) thus ( f = chi (X,C) implies ( dom f = C & ( for c being Element of C holds ( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) ) ) by FUNCT_3:def_3; ::_thesis: ( dom f = C & ( for c being Element of C holds ( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ) implies f = chi (X,C) ) assume that A1: dom f = C and A2: for c being Element of C holds ( ( c in X implies f . c = 1 ) & ( not c in X implies f . c = 0 ) ) ; ::_thesis: f = chi (X,C) for x being set st x in C holds ( ( x in X implies f . x = 1 ) & ( not x in X implies f . x = 0 ) ) by A2; hence f = chi (X,C) by A1, FUNCT_3:def_3; ::_thesis: verum end; theorem :: RFUNCT_1:62 for X being set for C being non empty set holds chi (X,C) is total ; theorem :: RFUNCT_1:63 for X being set for C being non empty set for c being Element of C holds ( c in X iff (chi (X,C)) . c = 1 ) by Th61; theorem :: RFUNCT_1:64 for X being set for C being non empty set for c being Element of C holds ( not c in X iff (chi (X,C)) . c = 0 ) by Th61; theorem :: RFUNCT_1:65 for X being set for C being non empty set for c being Element of C holds ( c in C \ X iff (chi (X,C)) . c = 0 ) proof let X be set ; ::_thesis: for C being non empty set for c being Element of C holds ( c in C \ X iff (chi (X,C)) . c = 0 ) let C be non empty set ; ::_thesis: for c being Element of C holds ( c in C \ X iff (chi (X,C)) . c = 0 ) let c be Element of C; ::_thesis: ( c in C \ X iff (chi (X,C)) . c = 0 ) thus ( c in C \ X implies (chi (X,C)) . c = 0 ) ::_thesis: ( (chi (X,C)) . c = 0 implies c in C \ X ) proof assume c in C \ X ; ::_thesis: (chi (X,C)) . c = 0 then not c in X by XBOOLE_0:def_5; hence (chi (X,C)) . c = 0 by Th61; ::_thesis: verum end; assume (chi (X,C)) . c = 0 ; ::_thesis: c in C \ X then not c in X by Th61; hence c in C \ X by XBOOLE_0:def_5; ::_thesis: verum end; theorem :: RFUNCT_1:66 for C being non empty set for c being Element of C holds (chi (C,C)) . c = 1 by Th61; theorem Th67: :: RFUNCT_1:67 for X being set for C being non empty set for c being Element of C holds ( (chi (X,C)) . c <> 1 iff (chi (X,C)) . c = 0 ) proof let X be set ; ::_thesis: for C being non empty set for c being Element of C holds ( (chi (X,C)) . c <> 1 iff (chi (X,C)) . c = 0 ) let C be non empty set ; ::_thesis: for c being Element of C holds ( (chi (X,C)) . c <> 1 iff (chi (X,C)) . c = 0 ) let c be Element of C; ::_thesis: ( (chi (X,C)) . c <> 1 iff (chi (X,C)) . c = 0 ) thus ( (chi (X,C)) . c <> 1 implies (chi (X,C)) . c = 0 ) ::_thesis: ( (chi (X,C)) . c = 0 implies (chi (X,C)) . c <> 1 ) proof c in C ; then c in dom (chi (X,C)) by Th61; then A1: (chi (X,C)) . c in rng (chi (X,C)) by FUNCT_1:def_3; A2: rng (chi (X,C)) c= {0,1} by FUNCT_3:39; assume (chi (X,C)) . c <> 1 ; ::_thesis: (chi (X,C)) . c = 0 hence (chi (X,C)) . c = 0 by A1, A2, TARSKI:def_2; ::_thesis: verum end; assume that A3: (chi (X,C)) . c = 0 and A4: (chi (X,C)) . c = 1 ; ::_thesis: contradiction thus contradiction by A3, A4; ::_thesis: verum end; theorem :: RFUNCT_1:68 for X, Y being set for C being non empty set st X misses Y holds (chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C) proof let X, Y be set ; ::_thesis: for C being non empty set st X misses Y holds (chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C) let C be non empty set ; ::_thesis: ( X misses Y implies (chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C) ) assume A1: X /\ Y = {} ; :: according to XBOOLE_0:def_7 ::_thesis: (chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C) A2: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((chi_(X,C))_+_(chi_(Y,C)))_holds_ ((chi_(X,C))_+_(chi_(Y,C)))_._c_=_(chi_((X_\/_Y),C))_._c let c be Element of C; ::_thesis: ( c in dom ((chi (X,C)) + (chi (Y,C))) implies ((chi (X,C)) + (chi (Y,C))) . c = (chi ((X \/ Y),C)) . c ) assume A3: c in dom ((chi (X,C)) + (chi (Y,C))) ; ::_thesis: ((chi (X,C)) + (chi (Y,C))) . c = (chi ((X \/ Y),C)) . c now__::_thesis:_((chi_(X,C))_._c)_+_((chi_(Y,C))_._c)_=_(chi_((X_\/_Y),C))_._c percases ( c in X or not c in X ) ; supposeA4: c in X ; ::_thesis: ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c then not c in Y by A1, XBOOLE_0:def_4; then A5: (chi (Y,C)) . c = 0 by Th61; A6: c in X \/ Y by A4, XBOOLE_0:def_3; (chi (X,C)) . c = 1 by A4, Th61; hence ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c by A5, A6, Th61; ::_thesis: verum end; supposeA7: not c in X ; ::_thesis: ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c then A8: (chi (X,C)) . c = 0 by Th61; now__::_thesis:_((chi_(X,C))_._c)_+_((chi_(Y,C))_._c)_=_(chi_((X_\/_Y),C))_._c percases ( c in Y or not c in Y ) ; supposeA9: c in Y ; ::_thesis: ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c then A10: c in X \/ Y by XBOOLE_0:def_3; (chi (Y,C)) . c = 1 by A9, Th61; hence ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c by A8, A10, Th61; ::_thesis: verum end; supposeA11: not c in Y ; ::_thesis: ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c then A12: not c in X \/ Y by A7, XBOOLE_0:def_3; (chi (Y,C)) . c = 0 by A11, Th61; hence ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c by A8, A12, Th61; ::_thesis: verum end; end; end; hence ((chi (X,C)) . c) + ((chi (Y,C)) . c) = (chi ((X \/ Y),C)) . c ; ::_thesis: verum end; end; end; hence ((chi (X,C)) + (chi (Y,C))) . c = (chi ((X \/ Y),C)) . c by A3, VALUED_1:def_1; ::_thesis: verum end; dom ((chi (X,C)) + (chi (Y,C))) = (dom (chi (X,C))) /\ (dom (chi (Y,C))) by VALUED_1:def_1 .= C /\ (dom (chi (Y,C))) by Th61 .= C /\ C by Th61 .= dom (chi ((X \/ Y),C)) by Th61 ; hence (chi (X,C)) + (chi (Y,C)) = chi ((X \/ Y),C) by A2, PARTFUN1:5; ::_thesis: verum end; theorem :: RFUNCT_1:69 for X, Y being set for C being non empty set holds (chi (X,C)) (#) (chi (Y,C)) = chi ((X /\ Y),C) proof let X, Y be set ; ::_thesis: for C being non empty set holds (chi (X,C)) (#) (chi (Y,C)) = chi ((X /\ Y),C) let C be non empty set ; ::_thesis: (chi (X,C)) (#) (chi (Y,C)) = chi ((X /\ Y),C) A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((chi_(X,C))_(#)_(chi_(Y,C)))_holds_ ((chi_(X,C))_(#)_(chi_(Y,C)))_._c_=_(chi_((X_/\_Y),C))_._c let c be Element of C; ::_thesis: ( c in dom ((chi (X,C)) (#) (chi (Y,C))) implies ((chi (X,C)) (#) (chi (Y,C))) . c = (chi ((X /\ Y),C)) . c ) assume c in dom ((chi (X,C)) (#) (chi (Y,C))) ; ::_thesis: ((chi (X,C)) (#) (chi (Y,C))) . c = (chi ((X /\ Y),C)) . c now__::_thesis:_((chi_(X,C))_._c)_*_((chi_(Y,C))_._c)_=_(chi_((X_/\_Y),C))_._c percases ( ((chi (X,C)) . c) * ((chi (Y,C)) . c) = 0 or ((chi (X,C)) . c) * ((chi (Y,C)) . c) <> 0 ) ; supposeA2: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = 0 ; ::_thesis: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c now__::_thesis:_((chi_(X,C))_._c)_*_((chi_(Y,C))_._c)_=_(chi_((X_/\_Y),C))_._c percases ( (chi (X,C)) . c = 0 or (chi (Y,C)) . c = 0 ) by A2; suppose (chi (X,C)) . c = 0 ; ::_thesis: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c then not c in X by Th61; then not c in X /\ Y by XBOOLE_0:def_4; hence ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c by A2, Th61; ::_thesis: verum end; suppose (chi (Y,C)) . c = 0 ; ::_thesis: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c then not c in Y by Th61; then not c in X /\ Y by XBOOLE_0:def_4; hence ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c by A2, Th61; ::_thesis: verum end; end; end; hence ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c ; ::_thesis: verum end; supposeA3: ((chi (X,C)) . c) * ((chi (Y,C)) . c) <> 0 ; ::_thesis: ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c then A4: (chi (Y,C)) . c <> 0 ; then A5: (chi (Y,C)) . c = 1 by Th67; A6: c in Y by A4, Th61; A7: (chi (X,C)) . c <> 0 by A3; then c in X by Th61; then A8: c in X /\ Y by A6, XBOOLE_0:def_4; (chi (X,C)) . c = 1 by A7, Th67; hence ((chi (X,C)) . c) * ((chi (Y,C)) . c) = (chi ((X /\ Y),C)) . c by A5, A8, Th61; ::_thesis: verum end; end; end; hence ((chi (X,C)) (#) (chi (Y,C))) . c = (chi ((X /\ Y),C)) . c by VALUED_1:5; ::_thesis: verum end; dom ((chi (X,C)) (#) (chi (Y,C))) = (dom (chi (X,C))) /\ (dom (chi (Y,C))) by VALUED_1:def_4 .= C /\ (dom (chi (Y,C))) by Th61 .= C /\ C by Th61 .= dom (chi ((X /\ Y),C)) by Th61 ; hence (chi (X,C)) (#) (chi (Y,C)) = chi ((X /\ Y),C) by A1, PARTFUN1:5; ::_thesis: verum end; theorem Th70: :: RFUNCT_1:70 for Y being set for f being real-valued Function holds ( f | Y is bounded_above iff ex r being real number st for c being set st c in Y /\ (dom f) holds f . c <= r ) proof let Y be set ; ::_thesis: for f being real-valued Function holds ( f | Y is bounded_above iff ex r being real number st for c being set st c in Y /\ (dom f) holds f . c <= r ) let f be real-valued Function; ::_thesis: ( f | Y is bounded_above iff ex r being real number st for c being set st c in Y /\ (dom f) holds f . c <= r ) thus ( f | Y is bounded_above implies ex r being real number st for c being set st c in Y /\ (dom f) holds f . c <= r ) ::_thesis: ( ex r being real number st for c being set st c in Y /\ (dom f) holds f . c <= r implies f | Y is bounded_above ) proof given r being real number such that A1: for p being set st p in dom (f | Y) holds (f | Y) . p < r ; :: according to SEQ_2:def_1 ::_thesis: ex r being real number st for c being set st c in Y /\ (dom f) holds f . c <= r take r ; ::_thesis: for c being set st c in Y /\ (dom f) holds f . c <= r let c be set ; ::_thesis: ( c in Y /\ (dom f) implies f . c <= r ) assume c in Y /\ (dom f) ; ::_thesis: f . c <= r then A2: c in dom (f | Y) by RELAT_1:61; then (f | Y) . c < r by A1; hence f . c <= r by A2, FUNCT_1:47; ::_thesis: verum end; given r being real number such that A3: for c being set st c in Y /\ (dom f) holds f . c <= r ; ::_thesis: f | Y is bounded_above reconsider r1 = r + 1 as real number ; take r1 ; :: according to SEQ_2:def_1 ::_thesis: for b1 being set holds ( not b1 in dom (f | Y) or not r1 <= K260((f | Y),b1) ) let p be set ; ::_thesis: ( not p in dom (f | Y) or not r1 <= K260((f | Y),p) ) assume A4: p in dom (f | Y) ; ::_thesis: not r1 <= K260((f | Y),p) then p in Y /\ (dom f) by RELAT_1:61; then f . p <= r by A3; then A5: (f | Y) . p <= r by A4, FUNCT_1:47; r < r1 by XREAL_1:29; hence not r1 <= K260((f | Y),p) by A5, XXREAL_0:2; ::_thesis: verum end; theorem Th71: :: RFUNCT_1:71 for Y being set for f being real-valued Function holds ( f | Y is bounded_below iff ex r being real number st for c being set st c in Y /\ (dom f) holds r <= f . c ) proof let Y be set ; ::_thesis: for f being real-valued Function holds ( f | Y is bounded_below iff ex r being real number st for c being set st c in Y /\ (dom f) holds r <= f . c ) let f be real-valued Function; ::_thesis: ( f | Y is bounded_below iff ex r being real number st for c being set st c in Y /\ (dom f) holds r <= f . c ) thus ( f | Y is bounded_below implies ex r being real number st for c being set st c in Y /\ (dom f) holds r <= f . c ) ::_thesis: ( ex r being real number st for c being set st c in Y /\ (dom f) holds r <= f . c implies f | Y is bounded_below ) proof given r being real number such that A1: for p being set st p in dom (f | Y) holds r < (f | Y) . p ; :: according to SEQ_2:def_2 ::_thesis: ex r being real number st for c being set st c in Y /\ (dom f) holds r <= f . c take r ; ::_thesis: for c being set st c in Y /\ (dom f) holds r <= f . c let c be set ; ::_thesis: ( c in Y /\ (dom f) implies r <= f . c ) assume c in Y /\ (dom f) ; ::_thesis: r <= f . c then A2: c in dom (f | Y) by RELAT_1:61; then r < (f | Y) . c by A1; hence r <= f . c by A2, FUNCT_1:47; ::_thesis: verum end; given r being real number such that A3: for c being set st c in Y /\ (dom f) holds r <= f . c ; ::_thesis: f | Y is bounded_below reconsider r1 = r - 1 as real number ; take r1 ; :: according to SEQ_2:def_2 ::_thesis: for b1 being set holds ( not b1 in dom (f | Y) or not K260((f | Y),b1) <= r1 ) let p be set ; ::_thesis: ( not p in dom (f | Y) or not K260((f | Y),p) <= r1 ) assume A4: p in dom (f | Y) ; ::_thesis: not K260((f | Y),p) <= r1 then p in Y /\ (dom f) by RELAT_1:61; then r <= f . p by A3; then A5: r <= (f | Y) . p by A4, FUNCT_1:47; r1 < r by XREAL_1:44; hence not K260((f | Y),p) <= r1 by A5, XXREAL_0:2; ::_thesis: verum end; theorem Th72: :: RFUNCT_1:72 for f being real-valued Function holds ( f is bounded iff ex r being real number st for c being set st c in dom f holds abs (f . c) <= r ) proof let f be real-valued Function; ::_thesis: ( f is bounded iff ex r being real number st for c being set st c in dom f holds abs (f . c) <= r ) thus ( f is bounded implies ex r being real number st for c being set st c in dom f holds abs (f . c) <= r ) ::_thesis: ( ex r being real number st for c being set st c in dom f holds abs (f . c) <= r implies f is bounded ) proof assume A1: f is bounded ; ::_thesis: ex r being real number st for c being set st c in dom f holds abs (f . c) <= r then consider r1 being real number such that A2: for c being set st c in dom f holds f . c < r1 by SEQ_2:def_1; consider r2 being real number such that A3: for c being set st c in dom f holds r2 < f . c by A1, SEQ_2:def_2; take g = (abs r1) + (abs r2); ::_thesis: for c being set st c in dom f holds abs (f . c) <= g let c be set ; ::_thesis: ( c in dom f implies abs (f . c) <= g ) assume A4: c in dom f ; ::_thesis: abs (f . c) <= g A5: 0 <= abs r2 by COMPLEX1:46; r1 <= abs r1 by ABSVALUE:4; then f . c <= abs r1 by A2, A4, XXREAL_0:2; then A6: (f . c) + 0 <= (abs r1) + (abs r2) by A5, XREAL_1:7; A7: 0 <= abs r1 by COMPLEX1:46; - (abs r2) <= r2 by ABSVALUE:4; then - (abs r2) <= f . c by A3, A4, XXREAL_0:2; then A8: (- (abs r1)) + (- (abs r2)) <= 0 + (f . c) by A7, XREAL_1:7; (- (abs r1)) + (- (abs r2)) = - g ; hence abs (f . c) <= g by A6, A8, ABSVALUE:5; ::_thesis: verum end; given r being real number such that A9: for c being set st c in dom f holds abs (f . c) <= r ; ::_thesis: f is bounded thus f is bounded_above :: according to SEQ_2:def_8 ::_thesis: f is bounded_below proof take r + 1 ; :: according to SEQ_2:def_1 ::_thesis: for b1 being set holds ( not b1 in dom f or not r + 1 <= K260(f,b1) ) let c be set ; ::_thesis: ( not c in dom f or not r + 1 <= K260(f,c) ) assume c in dom f ; ::_thesis: not r + 1 <= K260(f,c) then A10: abs (f . c) < r + 1 by A9, XREAL_1:39; f . c <= abs (f . c) by ABSVALUE:4; hence not r + 1 <= K260(f,c) by A10, XXREAL_0:2; ::_thesis: verum end; take - (r + 1) ; :: according to SEQ_2:def_2 ::_thesis: for b1 being set holds ( not b1 in dom f or not K260(f,b1) <= - (r + 1) ) let c be set ; ::_thesis: ( not c in dom f or not K260(f,c) <= - (r + 1) ) assume c in dom f ; ::_thesis: not K260(f,c) <= - (r + 1) then abs (f . c) < r + 1 by A9, XREAL_1:39; then A11: - (r + 1) < - (abs (f . c)) by XREAL_1:24; - (abs (f . c)) <= f . c by ABSVALUE:4; hence not K260(f,c) <= - (r + 1) by A11, XXREAL_0:2; ::_thesis: verum end; theorem :: RFUNCT_1:73 for Y being set for f being real-valued Function holds ( f | Y is bounded iff ex r being real number st for c being set st c in Y /\ (dom f) holds abs (f . c) <= r ) proof let Y be set ; ::_thesis: for f being real-valued Function holds ( f | Y is bounded iff ex r being real number st for c being set st c in Y /\ (dom f) holds abs (f . c) <= r ) let f be real-valued Function; ::_thesis: ( f | Y is bounded iff ex r being real number st for c being set st c in Y /\ (dom f) holds abs (f . c) <= r ) thus ( f | Y is bounded implies ex r being real number st for c being set st c in Y /\ (dom f) holds abs (f . c) <= r ) ::_thesis: ( ex r being real number st for c being set st c in Y /\ (dom f) holds abs (f . c) <= r implies f | Y is bounded ) proof assume A1: f | Y is bounded ; ::_thesis: ex r being real number st for c being set st c in Y /\ (dom f) holds abs (f . c) <= r then consider r1 being real number such that A2: for c being set st c in Y /\ (dom f) holds f . c <= r1 by Th70; consider r2 being real number such that A3: for c being set st c in Y /\ (dom f) holds r2 <= f . c by A1, Th71; take g = (abs r1) + (abs r2); ::_thesis: for c being set st c in Y /\ (dom f) holds abs (f . c) <= g A4: r1 <= abs r1 by ABSVALUE:4; let c be set ; ::_thesis: ( c in Y /\ (dom f) implies abs (f . c) <= g ) assume A5: c in Y /\ (dom f) ; ::_thesis: abs (f . c) <= g f . c <= r1 by A2, A5; then A6: f . c <= abs r1 by A4, XXREAL_0:2; A7: - (abs r2) <= r2 by ABSVALUE:4; r2 <= f . c by A3, A5; then A8: - (abs r2) <= f . c by A7, XXREAL_0:2; 0 <= abs r1 by COMPLEX1:46; then A9: (- (abs r1)) + (- (abs r2)) <= 0 + (f . c) by A8, XREAL_1:7; 0 <= abs r2 by COMPLEX1:46; then A10: (f . c) + 0 <= (abs r1) + (abs r2) by A6, XREAL_1:7; (- (abs r1)) + (- (abs r2)) = - g ; hence abs (f . c) <= g by A10, A9, ABSVALUE:5; ::_thesis: verum end; given r being real number such that A11: for c being set st c in Y /\ (dom f) holds abs (f . c) <= r ; ::_thesis: f | Y is bounded now__::_thesis:_for_c_being_set_st_c_in_Y_/\_(dom_f)_holds_ -_r_<=_f_._c let c be set ; ::_thesis: ( c in Y /\ (dom f) implies - r <= f . c ) assume c in Y /\ (dom f) ; ::_thesis: - r <= f . c then abs (f . c) <= r by A11; then A12: - r <= - (abs (f . c)) by XREAL_1:24; - (abs (f . c)) <= f . c by ABSVALUE:4; hence - r <= f . c by A12, XXREAL_0:2; ::_thesis: verum end; then A13: f | Y is bounded_below by Th71; now__::_thesis:_for_c_being_set_st_c_in_Y_/\_(dom_f)_holds_ f_._c_<=_r let c be set ; ::_thesis: ( c in Y /\ (dom f) implies f . c <= r ) assume c in Y /\ (dom f) ; ::_thesis: f . c <= r then A14: abs (f . c) <= r by A11; f . c <= abs (f . c) by ABSVALUE:4; hence f . c <= r by A14, XXREAL_0:2; ::_thesis: verum end; then f | Y is bounded_above by Th70; hence f | Y is bounded by A13; ::_thesis: verum end; theorem :: RFUNCT_1:74 for Y, X being set for f being real-valued Function holds ( ( Y c= X & f | X is bounded_above implies f | Y is bounded_above ) & ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) & ( Y c= X & f | X is bounded implies f | Y is bounded ) ) proof let Y, X be set ; ::_thesis: for f being real-valued Function holds ( ( Y c= X & f | X is bounded_above implies f | Y is bounded_above ) & ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) & ( Y c= X & f | X is bounded implies f | Y is bounded ) ) let f be real-valued Function; ::_thesis: ( ( Y c= X & f | X is bounded_above implies f | Y is bounded_above ) & ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) & ( Y c= X & f | X is bounded implies f | Y is bounded ) ) thus A1: ( Y c= X & f | X is bounded_above implies f | Y is bounded_above ) ::_thesis: ( ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) & ( Y c= X & f | X is bounded implies f | Y is bounded ) ) proof assume that A2: Y c= X and A3: f | X is bounded_above ; ::_thesis: f | Y is bounded_above consider r being real number such that A4: for c being set st c in X /\ (dom f) holds f . c <= r by A3, Th70; now__::_thesis:_ex_r_being_real_number_st_ for_c_being_set_st_c_in_Y_/\_(dom_f)_holds_ f_._c_<=_r take r = r; ::_thesis: for c being set st c in Y /\ (dom f) holds f . c <= r let c be set ; ::_thesis: ( c in Y /\ (dom f) implies f . c <= r ) assume A5: c in Y /\ (dom f) ; ::_thesis: f . c <= r then A6: c in dom f by XBOOLE_0:def_4; c in Y by A5, XBOOLE_0:def_4; then c in X /\ (dom f) by A2, A6, XBOOLE_0:def_4; hence f . c <= r by A4; ::_thesis: verum end; hence f | Y is bounded_above by Th70; ::_thesis: verum end; thus A7: ( Y c= X & f | X is bounded_below implies f | Y is bounded_below ) ::_thesis: ( Y c= X & f | X is bounded implies f | Y is bounded ) proof assume that A8: Y c= X and A9: f | X is bounded_below ; ::_thesis: f | Y is bounded_below consider r being real number such that A10: for c being set st c in X /\ (dom f) holds r <= f . c by A9, Th71; now__::_thesis:_ex_r_being_real_number_st_ for_c_being_set_st_c_in_Y_/\_(dom_f)_holds_ r_<=_f_._c take r = r; ::_thesis: for c being set st c in Y /\ (dom f) holds r <= f . c let c be set ; ::_thesis: ( c in Y /\ (dom f) implies r <= f . c ) assume A11: c in Y /\ (dom f) ; ::_thesis: r <= f . c then A12: c in dom f by XBOOLE_0:def_4; c in Y by A11, XBOOLE_0:def_4; then c in X /\ (dom f) by A8, A12, XBOOLE_0:def_4; hence r <= f . c by A10; ::_thesis: verum end; hence f | Y is bounded_below by Th71; ::_thesis: verum end; assume that A13: Y c= X and A14: f | X is bounded ; ::_thesis: f | Y is bounded thus f | Y is bounded by A1, A7, A13, A14; ::_thesis: verum end; theorem :: RFUNCT_1:75 for X, Y being set for f being real-valued Function st f | X is bounded_above & f | Y is bounded_below holds f | (X /\ Y) is bounded proof let X, Y be set ; ::_thesis: for f being real-valued Function st f | X is bounded_above & f | Y is bounded_below holds f | (X /\ Y) is bounded let f be real-valued Function; ::_thesis: ( f | X is bounded_above & f | Y is bounded_below implies f | (X /\ Y) is bounded ) assume that A1: f | X is bounded_above and A2: f | Y is bounded_below ; ::_thesis: f | (X /\ Y) is bounded consider r1 being real number such that A3: for c being set st c in X /\ (dom f) holds f . c <= r1 by A1, Th70; now__::_thesis:_for_c_being_set_st_c_in_(X_/\_Y)_/\_(dom_f)_holds_ f_._c_<=_r1 let c be set ; ::_thesis: ( c in (X /\ Y) /\ (dom f) implies f . c <= r1 ) assume A4: c in (X /\ Y) /\ (dom f) ; ::_thesis: f . c <= r1 then c in X /\ Y by XBOOLE_0:def_4; then A5: c in X by XBOOLE_0:def_4; c in dom f by A4, XBOOLE_0:def_4; then c in X /\ (dom f) by A5, XBOOLE_0:def_4; hence f . c <= r1 by A3; ::_thesis: verum end; hence f | (X /\ Y) is bounded_above by Th70; :: according to SEQ_2:def_8 ::_thesis: f | (X /\ Y) is bounded_below consider r2 being real number such that A6: for c being set st c in Y /\ (dom f) holds r2 <= f . c by A2, Th71; now__::_thesis:_for_c_being_set_st_c_in_(X_/\_Y)_/\_(dom_f)_holds_ r2_<=_f_._c let c be set ; ::_thesis: ( c in (X /\ Y) /\ (dom f) implies r2 <= f . c ) assume A7: c in (X /\ Y) /\ (dom f) ; ::_thesis: r2 <= f . c then c in X /\ Y by XBOOLE_0:def_4; then A8: c in Y by XBOOLE_0:def_4; c in dom f by A7, XBOOLE_0:def_4; then c in Y /\ (dom f) by A8, XBOOLE_0:def_4; hence r2 <= f . c by A6; ::_thesis: verum end; hence f | (X /\ Y) is bounded_below by Th71; ::_thesis: verum end; registration cluster Relation-like Function-like constant real-valued -> real-valued bounded for set ; coherence for b1 being real-valued Function st b1 is constant holds b1 is bounded proof let f be real-valued Function; ::_thesis: ( f is constant implies f is bounded ) percases ( f is empty or not f is empty ) ; supposeA1: f is empty ; ::_thesis: ( f is constant implies f is bounded ) reconsider z = 0 as real number ; assume f is constant ; ::_thesis: f is bounded thus f is bounded_above :: according to SEQ_2:def_8 ::_thesis: f is bounded_below proof take z ; :: according to SEQ_2:def_1 ::_thesis: for b1 being set holds ( not b1 in dom f or not z <= K260(f,b1) ) let x be set ; ::_thesis: ( not x in dom f or not z <= K260(f,x) ) thus ( not x in dom f or not z <= K260(f,x) ) by A1; ::_thesis: verum end; take z ; :: according to SEQ_2:def_2 ::_thesis: for b1 being set holds ( not b1 in dom f or not K260(f,b1) <= z ) let x be set ; ::_thesis: ( not x in dom f or not K260(f,x) <= z ) thus ( not x in dom f or not K260(f,x) <= z ) by A1; ::_thesis: verum end; supposeA2: not f is empty ; ::_thesis: ( f is constant implies f is bounded ) assume f is constant ; ::_thesis: f is bounded then consider r being real number such that A3: for c being set st c in dom f holds f . c = r by A2, VALUED_0:15; thus f is bounded_above :: according to SEQ_2:def_8 ::_thesis: f is bounded_below proof take r + 1 ; :: according to SEQ_2:def_1 ::_thesis: for b1 being set holds ( not b1 in dom f or not r + 1 <= K260(f,b1) ) let y be set ; ::_thesis: ( not y in dom f or not r + 1 <= K260(f,y) ) assume y in dom f ; ::_thesis: not r + 1 <= K260(f,y) then f . y = r by A3; hence not r + 1 <= K260(f,y) by XREAL_1:39; ::_thesis: verum end; take r - 1 ; :: according to SEQ_2:def_2 ::_thesis: for b1 being set holds ( not b1 in dom f or not K260(f,b1) <= r - 1 ) let y be set ; ::_thesis: ( not y in dom f or not K260(f,y) <= r - 1 ) assume y in dom f ; ::_thesis: not K260(f,y) <= r - 1 then f . y = r by A3; hence not K260(f,y) <= r - 1 by XREAL_1:231; ::_thesis: verum end; end; end; end; theorem :: RFUNCT_1:76 for X being set for f being real-valued Function st X misses dom f holds f | X is bounded proof let X be set ; ::_thesis: for f being real-valued Function st X misses dom f holds f | X is bounded let f be real-valued Function; ::_thesis: ( X misses dom f implies f | X is bounded ) assume X /\ (dom f) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: f | X is bounded then dom (f | X) = {} by RELAT_1:61; then f | X = {} ; hence f | X is bounded ; ::_thesis: verum end; theorem :: RFUNCT_1:77 for Y being set for f being real-valued Function holds (0 (#) f) | Y is bounded proof let Y be set ; ::_thesis: for f being real-valued Function holds (0 (#) f) | Y is bounded let f be real-valued Function; ::_thesis: (0 (#) f) | Y is bounded reconsider p1 = 0 as Real ; set r = 0 ; now__::_thesis:_ex_p_being_Real_st_ for_c_being_set_st_c_in_Y_/\_(dom_(0_(#)_f))_holds_ (0_(#)_f)_._c_<=_p take p = p1; ::_thesis: for c being set st c in Y /\ (dom (0 (#) f)) holds (0 (#) f) . c <= p let c be set ; ::_thesis: ( c in Y /\ (dom (0 (#) f)) implies (0 (#) f) . c <= p ) assume c in Y /\ (dom (0 (#) f)) ; ::_thesis: (0 (#) f) . c <= p then A1: c in dom (0 (#) f) by XBOOLE_0:def_4; 0 * (f . c) <= 0 ; hence (0 (#) f) . c <= p by A1, VALUED_1:def_5; ::_thesis: verum end; hence (0 (#) f) | Y is bounded_above by Th70; :: according to SEQ_2:def_8 ::_thesis: (0 (#) f) | Y is bounded_below now__::_thesis:_ex_p_being_Real_st_ for_c_being_set_st_c_in_Y_/\_(dom_(0_(#)_f))_holds_ p_<=_(0_(#)_f)_._c take p = p1; ::_thesis: for c being set st c in Y /\ (dom (0 (#) f)) holds p <= (0 (#) f) . c let c be set ; ::_thesis: ( c in Y /\ (dom (0 (#) f)) implies p <= (0 (#) f) . c ) assume c in Y /\ (dom (0 (#) f)) ; ::_thesis: p <= (0 (#) f) . c then A2: c in dom (0 (#) f) by XBOOLE_0:def_4; 0 <= 0 * (f . c) ; hence p <= (0 (#) f) . c by A2, VALUED_1:def_5; ::_thesis: verum end; hence (0 (#) f) | Y is bounded_below by Th71; ::_thesis: verum end; registration let f be real-valued bounded_above Function; let X be set ; clusterf | X -> real-valued bounded_above for real-valued Function; coherence for b1 being real-valued Function st b1 = f | X holds b1 is bounded_above proof consider r being real number such that A1: for y being set st y in dom f holds f . y < r by SEQ_2:def_1; f | X is bounded_above proof take r ; :: according to SEQ_2:def_1 ::_thesis: for b1 being set holds ( not b1 in dom (f | X) or not r <= K260((f | X),b1) ) let y be set ; ::_thesis: ( not y in dom (f | X) or not r <= K260((f | X),y) ) assume A2: y in dom (f | X) ; ::_thesis: not r <= K260((f | X),y) then y in dom f by RELAT_1:57; then f . y < r by A1; hence not r <= K260((f | X),y) by A2, FUNCT_1:47; ::_thesis: verum end; hence for b1 being real-valued Function st b1 = f | X holds b1 is bounded_above ; ::_thesis: verum end; end; registration let f be real-valued bounded_below Function; let X be set ; clusterf | X -> real-valued bounded_below for real-valued Function; coherence for b1 being real-valued Function st b1 = f | X holds b1 is bounded_below proof consider r being real number such that A1: for y being set st y in dom f holds r < f . y by SEQ_2:def_2; f | X is bounded_below proof take r ; :: according to SEQ_2:def_2 ::_thesis: for b1 being set holds ( not b1 in dom (f | X) or not K260((f | X),b1) <= r ) let y be set ; ::_thesis: ( not y in dom (f | X) or not K260((f | X),y) <= r ) assume A2: y in dom (f | X) ; ::_thesis: not K260((f | X),y) <= r then y in dom f by RELAT_1:57; then r < f . y by A1; hence not K260((f | X),y) <= r by A2, FUNCT_1:47; ::_thesis: verum end; hence for b1 being real-valued Function st b1 = f | X holds b1 is bounded_below ; ::_thesis: verum end; end; registration let f be real-valued bounded_above Function; let r be non negative real number ; clusterr (#) f -> real-valued bounded_above for real-valued Function; coherence for b1 being real-valued Function st b1 = r (#) f holds b1 is bounded_above proof consider r1 being real number such that A1: for c being set st c in dom f holds f . c < r1 by SEQ_2:def_1; now__::_thesis:_ex_p_being_Element_of_REAL_st_ for_c_being_set_st_c_in_dom_(r_(#)_f)_holds_ (r_(#)_f)_._c_<_p take p = (r * (abs r1)) + 1; ::_thesis: for c being set st c in dom (r (#) f) holds (r (#) f) . c < p let c be set ; ::_thesis: ( c in dom (r (#) f) implies (r (#) f) . c < p ) A2: r1 <= abs r1 by ABSVALUE:4; assume A3: c in dom (r (#) f) ; ::_thesis: (r (#) f) . c < p then c in dom f by VALUED_1:def_5; then f . c < abs r1 by A1, A2, XXREAL_0:2; then r * (f . c) <= (abs r1) * r by XREAL_1:64; then (r (#) f) . c <= (abs r1) * r by A3, VALUED_1:def_5; hence (r (#) f) . c < p by XREAL_1:39; ::_thesis: verum end; hence for b1 being real-valued Function st b1 = r (#) f holds b1 is bounded_above by SEQ_2:def_1; ::_thesis: verum end; end; registration let f be real-valued bounded_below Function; let r be non negative real number ; clusterr (#) f -> real-valued bounded_below for real-valued Function; coherence for b1 being real-valued Function st b1 = r (#) f holds b1 is bounded_below proof consider r1 being real number such that A1: for c being set st c in dom f holds r1 < f . c by SEQ_2:def_2; now__::_thesis:_ex_p_being_Element_of_REAL_st_ for_c_being_set_st_c_in_dom_(r_(#)_f)_holds_ (r_(#)_f)_._c_>_p take p = (r * (- (abs r1))) - 1; ::_thesis: for c being set st c in dom (r (#) f) holds (r (#) f) . c > p let c be set ; ::_thesis: ( c in dom (r (#) f) implies (r (#) f) . c > p ) A2: - (abs r1) <= r1 by ABSVALUE:4; assume A3: c in dom (r (#) f) ; ::_thesis: (r (#) f) . c > p then c in dom f by VALUED_1:def_5; then f . c >= - (abs r1) by A1, A2, XXREAL_0:2; then r * (f . c) >= (- (abs r1)) * r by XREAL_1:64; then (r (#) f) . c >= (- (abs r1)) * r by A3, VALUED_1:def_5; hence (r (#) f) . c > p by XREAL_1:231; ::_thesis: verum end; hence for b1 being real-valued Function st b1 = r (#) f holds b1 is bounded_below by SEQ_2:def_2; ::_thesis: verum end; end; registration let f be real-valued bounded_above Function; let r be non positive real number ; clusterr (#) f -> real-valued bounded_below for real-valued Function; coherence for b1 being real-valued Function st b1 = r (#) f holds b1 is bounded_below proof consider r1 being real number such that A1: for c being set st c in dom f holds f . c < r1 by SEQ_2:def_1; now__::_thesis:_ex_p_being_Element_of_REAL_st_ for_c_being_set_st_c_in_dom_(r_(#)_f)_holds_ p_<_(r_(#)_f)_._c take p = (r * (abs r1)) - 1; ::_thesis: for c being set st c in dom (r (#) f) holds p < (r (#) f) . c let c be set ; ::_thesis: ( c in dom (r (#) f) implies p < (r (#) f) . c ) A2: r1 <= abs r1 by ABSVALUE:4; assume A3: c in dom (r (#) f) ; ::_thesis: p < (r (#) f) . c then c in dom f by VALUED_1:def_5; then f . c <= abs r1 by A1, A2, XXREAL_0:2; then r * (abs r1) <= r * (f . c) by XREAL_1:65; then r * (abs r1) <= (r (#) f) . c by A3, VALUED_1:def_5; hence p < (r (#) f) . c by XREAL_1:231; ::_thesis: verum end; hence for b1 being real-valued Function st b1 = r (#) f holds b1 is bounded_below by SEQ_2:def_2; ::_thesis: verum end; end; registration let f be real-valued bounded_below Function; let r be non positive real number ; clusterr (#) f -> real-valued bounded_above for real-valued Function; coherence for b1 being real-valued Function st b1 = r (#) f holds b1 is bounded_above proof consider r1 being real number such that A1: for c being set st c in dom f holds r1 < f . c by SEQ_2:def_2; now__::_thesis:_ex_p_being_Element_of_REAL_st_ for_c_being_set_st_c_in_dom_(r_(#)_f)_holds_ (r_(#)_f)_._c_<_p take p = (r * (- (abs r1))) + 1; ::_thesis: for c being set st c in dom (r (#) f) holds (r (#) f) . c < p let c be set ; ::_thesis: ( c in dom (r (#) f) implies (r (#) f) . c < p ) A2: - (abs r1) <= r1 by ABSVALUE:4; assume A3: c in dom (r (#) f) ; ::_thesis: (r (#) f) . c < p then c in dom f by VALUED_1:def_5; then - (abs r1) <= f . c by A1, A2, XXREAL_0:2; then r * (f . c) <= r * (- (abs r1)) by XREAL_1:65; then (r (#) f) . c <= r * (- (abs r1)) by A3, VALUED_1:def_5; hence (r (#) f) . c < p by XREAL_1:39; ::_thesis: verum end; hence for b1 being real-valued Function st b1 = r (#) f holds b1 is bounded_above by SEQ_2:def_1; ::_thesis: verum end; end; theorem Th78: :: RFUNCT_1:78 for Y being set for r being real number for f being real-valued Function holds ( ( f | Y is bounded_above & 0 <= r implies (r (#) f) | Y is bounded_above ) & ( f | Y is bounded_above & r <= 0 implies (r (#) f) | Y is bounded_below ) ) proof let Y be set ; ::_thesis: for r being real number for f being real-valued Function holds ( ( f | Y is bounded_above & 0 <= r implies (r (#) f) | Y is bounded_above ) & ( f | Y is bounded_above & r <= 0 implies (r (#) f) | Y is bounded_below ) ) let r be real number ; ::_thesis: for f being real-valued Function holds ( ( f | Y is bounded_above & 0 <= r implies (r (#) f) | Y is bounded_above ) & ( f | Y is bounded_above & r <= 0 implies (r (#) f) | Y is bounded_below ) ) let f be real-valued Function; ::_thesis: ( ( f | Y is bounded_above & 0 <= r implies (r (#) f) | Y is bounded_above ) & ( f | Y is bounded_above & r <= 0 implies (r (#) f) | Y is bounded_below ) ) (r (#) f) | Y = r (#) (f | Y) by Th49; hence ( ( f | Y is bounded_above & 0 <= r implies (r (#) f) | Y is bounded_above ) & ( f | Y is bounded_above & r <= 0 implies (r (#) f) | Y is bounded_below ) ) ; ::_thesis: verum end; theorem Th79: :: RFUNCT_1:79 for Y being set for r being real number for f being real-valued Function holds ( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) ) proof let Y be set ; ::_thesis: for r being real number for f being real-valued Function holds ( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) ) let r be real number ; ::_thesis: for f being real-valued Function holds ( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) ) let f be real-valued Function; ::_thesis: ( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) ) (r (#) f) | Y = r (#) (f | Y) by Th49; hence ( ( f | Y is bounded_below & 0 <= r implies (r (#) f) | Y is bounded_below ) & ( f | Y is bounded_below & r <= 0 implies (r (#) f) | Y is bounded_above ) ) ; ::_thesis: verum end; theorem Th80: :: RFUNCT_1:80 for Y being set for r being real number for f being real-valued Function st f | Y is bounded holds (r (#) f) | Y is bounded proof let Y be set ; ::_thesis: for r being real number for f being real-valued Function st f | Y is bounded holds (r (#) f) | Y is bounded let r be real number ; ::_thesis: for f being real-valued Function st f | Y is bounded holds (r (#) f) | Y is bounded let f be real-valued Function; ::_thesis: ( f | Y is bounded implies (r (#) f) | Y is bounded ) assume A1: f | Y is bounded ; ::_thesis: (r (#) f) | Y is bounded percases ( 0 <= r or r <= 0 ) ; supposeA2: 0 <= r ; ::_thesis: (r (#) f) | Y is bounded hence (r (#) f) | Y is bounded_above by A1, Th78; :: according to SEQ_2:def_8 ::_thesis: (r (#) f) | Y is bounded_below thus (r (#) f) | Y is bounded_below by A1, A2, Th79; ::_thesis: verum end; supposeA3: r <= 0 ; ::_thesis: (r (#) f) | Y is bounded hence (r (#) f) | Y is bounded_above by A1, Th79; :: according to SEQ_2:def_8 ::_thesis: (r (#) f) | Y is bounded_below thus (r (#) f) | Y is bounded_below by A1, A3, Th78; ::_thesis: verum end; end; end; registration let f be real-valued Function; cluster|.f.| -> bounded_below ; coherence abs f is bounded_below proof now__::_thesis:_ex_p_being_real_number_st_ for_c_being_set_st_c_in_dom_(abs_f)_holds_ p_<_(abs_f)_._c reconsider p = - 1 as real number ; take p = p; ::_thesis: for c being set st c in dom (abs f) holds p < (abs f) . c let c be set ; ::_thesis: ( c in dom (abs f) implies p < (abs f) . c ) assume c in dom (abs f) ; ::_thesis: p < (abs f) . c 0 <= abs (f . c) by COMPLEX1:46; hence p < (abs f) . c by VALUED_1:18; ::_thesis: verum end; hence abs f is bounded_below by SEQ_2:def_2; ::_thesis: verum end; end; theorem :: RFUNCT_1:81 for X being set for f being real-valued Function holds (abs f) | X is bounded_below ; registration let f be real-valued bounded Function; cluster|.f.| -> real-valued bounded for real-valued Function; coherence for b1 being real-valued Function st b1 = abs f holds b1 is bounded proof consider r1 being real number such that A1: for c being set st c in dom f holds abs (f . c) <= r1 by Th72; now__::_thesis:_ex_r1_being_real_number_st_ for_c_being_set_st_c_in_dom_(abs_f)_holds_ abs_((abs_f)_._c)_<=_r1 take r1 = r1; ::_thesis: for c being set st c in dom (abs f) holds abs ((abs f) . c) <= r1 let c be set ; ::_thesis: ( c in dom (abs f) implies abs ((abs f) . c) <= r1 ) assume c in dom (abs f) ; ::_thesis: abs ((abs f) . c) <= r1 then c in dom f by VALUED_1:def_11; then abs (abs (f . c)) <= r1 by A1; hence abs ((abs f) . c) <= r1 by VALUED_1:18; ::_thesis: verum end; hence for b1 being real-valued Function st b1 = abs f holds b1 is bounded by Th72; ::_thesis: verum end; end; registration let f be real-valued bounded_above Function; cluster - f -> real-valued bounded_below for real-valued Function; coherence for b1 being real-valued Function st b1 = - f holds b1 is bounded_below ; end; theorem Th82: :: RFUNCT_1:82 for Y being set for f being real-valued Function st f | Y is bounded holds ( (abs f) | Y is bounded & (- f) | Y is bounded ) proof let Y be set ; ::_thesis: for f being real-valued Function st f | Y is bounded holds ( (abs f) | Y is bounded & (- f) | Y is bounded ) let f be real-valued Function; ::_thesis: ( f | Y is bounded implies ( (abs f) | Y is bounded & (- f) | Y is bounded ) ) assume A1: f | Y is bounded ; ::_thesis: ( (abs f) | Y is bounded & (- f) | Y is bounded ) (abs f) | Y = abs (f | Y) by Th46; hence (abs f) | Y is bounded by A1; ::_thesis: (- f) | Y is bounded thus (- f) | Y is bounded by A1, Th80; ::_thesis: verum end; registration let f1, f2 be real-valued bounded_above Function; clusterf1 + f2 -> real-valued bounded_above for real-valued Function; coherence for b1 being real-valued Function st b1 = f1 + f2 holds b1 is bounded_above proof consider r2 being real number such that A1: for c being set st c in dom f2 holds f2 . c < r2 by SEQ_2:def_1; consider r1 being real number such that A2: for c being set st c in dom f1 holds f1 . c < r1 by SEQ_2:def_1; now__::_thesis:_ex_r_being_set_st_ for_c_being_set_st_c_in_dom_(f1_+_f2)_holds_ (f1_+_f2)_._c_<_r take r = r1 + r2; ::_thesis: for c being set st c in dom (f1 + f2) holds (f1 + f2) . c < r let c be set ; ::_thesis: ( c in dom (f1 + f2) implies (f1 + f2) . c < r ) assume A3: c in dom (f1 + f2) ; ::_thesis: (f1 + f2) . c < r then A4: c in (dom f1) /\ (dom f2) by VALUED_1:def_1; then c in dom f1 by XBOOLE_0:def_4; then A5: f1 . c < r1 by A2; c in dom f2 by A4, XBOOLE_0:def_4; then (f1 . c) + (f2 . c) < r by A1, A5, XREAL_1:8; hence (f1 + f2) . c < r by A3, VALUED_1:def_1; ::_thesis: verum end; hence for b1 being real-valued Function st b1 = f1 + f2 holds b1 is bounded_above by SEQ_2:def_1; ::_thesis: verum end; end; registration let f1, f2 be real-valued bounded_below Function; clusterf1 + f2 -> real-valued bounded_below for real-valued Function; coherence for b1 being real-valued Function st b1 = f1 + f2 holds b1 is bounded_below proof consider r2 being real number such that A1: for c being set st c in dom f2 holds f2 . c > r2 by SEQ_2:def_2; consider r1 being real number such that A2: for c being set st c in dom f1 holds f1 . c > r1 by SEQ_2:def_2; now__::_thesis:_ex_r_being_set_st_ for_c_being_set_st_c_in_dom_(f1_+_f2)_holds_ (f1_+_f2)_._c_>_r take r = r1 + r2; ::_thesis: for c being set st c in dom (f1 + f2) holds (f1 + f2) . c > r let c be set ; ::_thesis: ( c in dom (f1 + f2) implies (f1 + f2) . c > r ) assume A3: c in dom (f1 + f2) ; ::_thesis: (f1 + f2) . c > r then A4: c in (dom f1) /\ (dom f2) by VALUED_1:def_1; then c in dom f1 by XBOOLE_0:def_4; then A5: f1 . c > r1 by A2; c in dom f2 by A4, XBOOLE_0:def_4; then (f1 . c) + (f2 . c) > r by A1, A5, XREAL_1:8; hence (f1 + f2) . c > r by A3, VALUED_1:def_1; ::_thesis: verum end; hence for b1 being real-valued Function st b1 = f1 + f2 holds b1 is bounded_below by SEQ_2:def_2; ::_thesis: verum end; end; theorem Th83: :: RFUNCT_1:83 for X, Y being set for f1, f2 being real-valued Function holds ( ( f1 | X is bounded_above & f2 | Y is bounded_above implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is bounded_below implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is bounded implies (f1 + f2) | (X /\ Y) is bounded ) ) proof let X, Y be set ; ::_thesis: for f1, f2 being real-valued Function holds ( ( f1 | X is bounded_above & f2 | Y is bounded_above implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is bounded_below implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is bounded implies (f1 + f2) | (X /\ Y) is bounded ) ) let f1, f2 be real-valued Function; ::_thesis: ( ( f1 | X is bounded_above & f2 | Y is bounded_above implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is bounded_below implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is bounded implies (f1 + f2) | (X /\ Y) is bounded ) ) (f1 + f2) | (X /\ Y) = (f1 | (X /\ Y)) + (f2 | (X /\ Y)) by Th44 .= (f1 | (X /\ Y)) + ((f2 | Y) | X) by RELAT_1:71 .= ((f1 | X) | Y) + ((f2 | Y) | X) by RELAT_1:71 ; hence ( ( f1 | X is bounded_above & f2 | Y is bounded_above implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is bounded_below implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is bounded implies (f1 + f2) | (X /\ Y) is bounded ) ) ; ::_thesis: verum end; registration let f1, f2 be real-valued bounded Function; clusterf1 (#) f2 -> real-valued bounded for real-valued Function; coherence for b1 being real-valued Function st b1 = f1 (#) f2 holds b1 is bounded proof consider r2 being real number such that A1: for c being set st c in dom f2 holds abs (f2 . c) <= r2 by Th72; consider r1 being real number such that A2: for c being set st c in dom f1 holds abs (f1 . c) <= r1 by Th72; now__::_thesis:_ex_r_being_set_st_ for_c_being_set_st_c_in_dom_(f1_(#)_f2)_holds_ abs_((f1_(#)_f2)_._c)_<=_r take r = r1 * r2; ::_thesis: for c being set st c in dom (f1 (#) f2) holds abs ((f1 (#) f2) . c) <= r let c be set ; ::_thesis: ( c in dom (f1 (#) f2) implies abs ((f1 (#) f2) . c) <= r ) A3: 0 <= abs (f2 . c) by COMPLEX1:46; assume c in dom (f1 (#) f2) ; ::_thesis: abs ((f1 (#) f2) . c) <= r then A4: c in (dom f1) /\ (dom f2) by VALUED_1:def_4; then c in dom f1 by XBOOLE_0:def_4; then A5: abs (f1 . c) <= r1 by A2; c in dom f2 by A4, XBOOLE_0:def_4; then A6: abs (f2 . c) <= r2 by A1; 0 <= abs (f1 . c) by COMPLEX1:46; then (abs (f1 . c)) * (abs (f2 . c)) <= r by A5, A6, A3, XREAL_1:66; then abs ((f1 . c) * (f2 . c)) <= r by COMPLEX1:65; hence abs ((f1 (#) f2) . c) <= r by VALUED_1:5; ::_thesis: verum end; hence for b1 being real-valued Function st b1 = f1 (#) f2 holds b1 is bounded by Th72; ::_thesis: verum end; end; theorem Th84: :: RFUNCT_1:84 for X, Y being set for f1, f2 being real-valued Function st f1 | X is bounded & f2 | Y is bounded holds ( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) proof let X, Y be set ; ::_thesis: for f1, f2 being real-valued Function st f1 | X is bounded & f2 | Y is bounded holds ( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) let f1, f2 be real-valued Function; ::_thesis: ( f1 | X is bounded & f2 | Y is bounded implies ( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) ) assume that A1: f1 | X is bounded and A2: f2 | Y is bounded ; ::_thesis: ( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) (f1 (#) f2) | (X /\ Y) = (f1 | (X /\ Y)) (#) (f2 | (X /\ Y)) by Th45 .= (f1 | (X /\ Y)) (#) ((f2 | Y) | X) by RELAT_1:71 .= ((f1 | X) | Y) (#) ((f2 | Y) | X) by RELAT_1:71 ; hence (f1 (#) f2) | (X /\ Y) is bounded by A1, A2; ::_thesis: (f1 - f2) | (X /\ Y) is bounded (- f2) | Y is bounded by A2, Th82; hence (f1 - f2) | (X /\ Y) is bounded by A1, Th83; ::_thesis: verum end; theorem Th85: :: RFUNCT_1:85 for X, Y being set for f being real-valued Function st f | X is bounded_above & f | Y is bounded_above holds f | (X \/ Y) is bounded_above proof let X, Y be set ; ::_thesis: for f being real-valued Function st f | X is bounded_above & f | Y is bounded_above holds f | (X \/ Y) is bounded_above let f be real-valued Function; ::_thesis: ( f | X is bounded_above & f | Y is bounded_above implies f | (X \/ Y) is bounded_above ) assume that A1: f | X is bounded_above and A2: f | Y is bounded_above ; ::_thesis: f | (X \/ Y) is bounded_above consider r1 being real number such that A3: for c being set st c in X /\ (dom f) holds f . c <= r1 by A1, Th70; consider r2 being real number such that A4: for c being set st c in Y /\ (dom f) holds f . c <= r2 by A2, Th70; now__::_thesis:_ex_r_being_Element_of_REAL_st_ for_c_being_set_st_c_in_(X_\/_Y)_/\_(dom_f)_holds_ f_._c_<=_r take r = (abs r1) + (abs r2); ::_thesis: for c being set st c in (X \/ Y) /\ (dom f) holds f . c <= r let c be set ; ::_thesis: ( c in (X \/ Y) /\ (dom f) implies f . c <= r ) assume A5: c in (X \/ Y) /\ (dom f) ; ::_thesis: f . c <= r then A6: c in dom f by XBOOLE_0:def_4; A7: c in X \/ Y by A5, XBOOLE_0:def_4; now__::_thesis:_f_._c_<=_r percases ( c in X or c in Y ) by A7, XBOOLE_0:def_3; suppose c in X ; ::_thesis: f . c <= r then c in X /\ (dom f) by A6, XBOOLE_0:def_4; then A8: f . c <= r1 by A3; A9: 0 <= abs r2 by COMPLEX1:46; r1 <= abs r1 by ABSVALUE:4; then f . c <= abs r1 by A8, XXREAL_0:2; then (f . c) + 0 <= r by A9, XREAL_1:7; hence f . c <= r ; ::_thesis: verum end; suppose c in Y ; ::_thesis: f . c <= r then c in Y /\ (dom f) by A6, XBOOLE_0:def_4; then A10: f . c <= r2 by A4; A11: 0 <= abs r1 by COMPLEX1:46; r2 <= abs r2 by ABSVALUE:4; then f . c <= abs r2 by A10, XXREAL_0:2; then 0 + (f . c) <= r by A11, XREAL_1:7; hence f . c <= r ; ::_thesis: verum end; end; end; hence f . c <= r ; ::_thesis: verum end; hence f | (X \/ Y) is bounded_above by Th70; ::_thesis: verum end; theorem Th86: :: RFUNCT_1:86 for X, Y being set for f being real-valued Function st f | X is bounded_below & f | Y is bounded_below holds f | (X \/ Y) is bounded_below proof let X, Y be set ; ::_thesis: for f being real-valued Function st f | X is bounded_below & f | Y is bounded_below holds f | (X \/ Y) is bounded_below let f be real-valued Function; ::_thesis: ( f | X is bounded_below & f | Y is bounded_below implies f | (X \/ Y) is bounded_below ) assume that A1: f | X is bounded_below and A2: f | Y is bounded_below ; ::_thesis: f | (X \/ Y) is bounded_below consider r1 being real number such that A3: for c being set st c in X /\ (dom f) holds r1 <= f . c by A1, Th71; consider r2 being real number such that A4: for c being set st c in Y /\ (dom f) holds r2 <= f . c by A2, Th71; now__::_thesis:_ex_r_being_Element_of_REAL_st_ for_c_being_set_st_c_in_(X_\/_Y)_/\_(dom_f)_holds_ r_<=_f_._c take r = (- (abs r1)) - (abs r2); ::_thesis: for c being set st c in (X \/ Y) /\ (dom f) holds r <= f . c let c be set ; ::_thesis: ( c in (X \/ Y) /\ (dom f) implies r <= f . c ) assume A5: c in (X \/ Y) /\ (dom f) ; ::_thesis: r <= f . c then A6: c in dom f by XBOOLE_0:def_4; A7: c in X \/ Y by A5, XBOOLE_0:def_4; now__::_thesis:_r_<=_f_._c percases ( c in X or c in Y ) by A7, XBOOLE_0:def_3; suppose c in X ; ::_thesis: r <= f . c then c in X /\ (dom f) by A6, XBOOLE_0:def_4; then A8: r1 <= f . c by A3; A9: 0 <= abs r2 by COMPLEX1:46; - (abs r1) <= r1 by ABSVALUE:4; then - (abs r1) <= f . c by A8, XXREAL_0:2; then r <= (f . c) - 0 by A9, XREAL_1:13; hence r <= f . c ; ::_thesis: verum end; suppose c in Y ; ::_thesis: r <= f . c then c in Y /\ (dom f) by A6, XBOOLE_0:def_4; then A10: r2 <= f . c by A4; A11: 0 <= abs r1 by COMPLEX1:46; - (abs r2) <= r2 by ABSVALUE:4; then - (abs r2) <= f . c by A10, XXREAL_0:2; then (- (abs r2)) - (abs r1) <= (f . c) - 0 by A11, XREAL_1:13; hence r <= f . c ; ::_thesis: verum end; end; end; hence r <= f . c ; ::_thesis: verum end; hence f | (X \/ Y) is bounded_below by Th71; ::_thesis: verum end; theorem :: RFUNCT_1:87 for X, Y being set for f being real-valued Function st f | X is bounded & f | Y is bounded holds f | (X \/ Y) is bounded proof let X, Y be set ; ::_thesis: for f being real-valued Function st f | X is bounded & f | Y is bounded holds f | (X \/ Y) is bounded let f be real-valued Function; ::_thesis: ( f | X is bounded & f | Y is bounded implies f | (X \/ Y) is bounded ) assume that A1: f | X is bounded and A2: f | Y is bounded ; ::_thesis: f | (X \/ Y) is bounded thus f | (X \/ Y) is bounded_above by A1, A2, Th85; :: according to SEQ_2:def_8 ::_thesis: f | (X \/ Y) is bounded_below thus f | (X \/ Y) is bounded_below by A1, A2, Th86; ::_thesis: verum end; registration let C be non empty set ; let f1, f2 be constant PartFunc of C,REAL; clusterf1 + f2 -> constant ; coherence f1 + f2 is constant proof consider r2 being Real such that A1: for c being Element of C st c in dom f2 holds f2 . c = r2 by PARTFUN2:def_1; consider r1 being Real such that A2: for c being Element of C st c in dom f1 holds f1 . c = r1 by PARTFUN2:def_1; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_+_f2)_holds_ (f1_+_f2)_._c_=_r1_+_r2 let c be Element of C; ::_thesis: ( c in dom (f1 + f2) implies (f1 + f2) . c = r1 + r2 ) assume A3: c in dom (f1 + f2) ; ::_thesis: (f1 + f2) . c = r1 + r2 then A4: c in (dom f1) /\ (dom f2) by VALUED_1:def_1; then A5: c in dom f1 by XBOOLE_0:def_4; A6: c in dom f2 by A4, XBOOLE_0:def_4; thus (f1 + f2) . c = (f1 . c) + (f2 . c) by A3, VALUED_1:def_1 .= (f1 . c) + r2 by A1, A6 .= r1 + r2 by A2, A5 ; ::_thesis: verum end; hence f1 + f2 is constant by PARTFUN2:def_1; ::_thesis: verum end; clusterf1 - f2 -> constant ; coherence f1 - f2 is constant proof consider r2 being Real such that A7: for c being Element of C st c in dom f2 holds f2 . c = r2 by PARTFUN2:def_1; consider r1 being Real such that A8: for c being Element of C st c in dom f1 holds f1 . c = r1 by PARTFUN2:def_1; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_f2)_holds_ (f1_-_f2)_._c_=_r1_-_r2 let c be Element of C; ::_thesis: ( c in dom (f1 - f2) implies (f1 - f2) . c = r1 - r2 ) assume A9: c in dom (f1 - f2) ; ::_thesis: (f1 - f2) . c = r1 - r2 then A10: c in (dom f1) /\ (dom f2) by VALUED_1:12; then A11: c in dom f1 by XBOOLE_0:def_4; A12: c in dom f2 by A10, XBOOLE_0:def_4; thus (f1 - f2) . c = (f1 . c) - (f2 . c) by A9, VALUED_1:13 .= (f1 . c) - r2 by A7, A12 .= r1 - r2 by A8, A11 ; ::_thesis: verum end; hence f1 - f2 is constant by PARTFUN2:def_1; ::_thesis: verum end; clusterf1 (#) f2 -> constant ; coherence f1 (#) f2 is constant proof consider r2 being Real such that A13: for c being Element of C st c in dom f2 holds f2 . c = r2 by PARTFUN2:def_1; consider r1 being Real such that A14: for c being Element of C st c in dom f1 holds f1 . c = r1 by PARTFUN2:def_1; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_(#)_f2)_holds_ (f1_(#)_f2)_._c_=_r1_*_r2 let c be Element of C; ::_thesis: ( c in dom (f1 (#) f2) implies (f1 (#) f2) . c = r1 * r2 ) assume A15: c in dom (f1 (#) f2) ; ::_thesis: (f1 (#) f2) . c = r1 * r2 then A16: c in (dom f1) /\ (dom f2) by VALUED_1:def_4; then A17: c in dom f1 by XBOOLE_0:def_4; A18: c in dom f2 by A16, XBOOLE_0:def_4; thus (f1 (#) f2) . c = (f1 . c) * (f2 . c) by A15, VALUED_1:def_4 .= (f1 . c) * r2 by A13, A18 .= r1 * r2 by A14, A17 ; ::_thesis: verum end; hence f1 (#) f2 is constant by PARTFUN2:def_1; ::_thesis: verum end; end; theorem :: RFUNCT_1:88 for X, Y being set for C being non empty set for f1, f2 being PartFunc of C,REAL st f1 | X is constant & f2 | Y is constant holds ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant ) proof let X, Y be set ; ::_thesis: for C being non empty set for f1, f2 being PartFunc of C,REAL st f1 | X is constant & f2 | Y is constant holds ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant ) let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,REAL st f1 | X is constant & f2 | Y is constant holds ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant ) let f1, f2 be PartFunc of C,REAL; ::_thesis: ( f1 | X is constant & f2 | Y is constant implies ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant ) ) assume that A1: f1 | X is constant and A2: f2 | Y is constant ; ::_thesis: ( (f1 + f2) | (X /\ Y) is constant & (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant ) consider r1 being Real such that A3: for c being Element of C st c in X /\ (dom f1) holds f1 . c = r1 by A1, PARTFUN2:57; consider r2 being Real such that A4: for c being Element of C st c in Y /\ (dom f2) holds f2 . c = r2 by A2, PARTFUN2:57; now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_+_f2))_holds_ (f1_+_f2)_._c_=_r1_+_r2 let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies (f1 + f2) . c = r1 + r2 ) assume A5: c in (X /\ Y) /\ (dom (f1 + f2)) ; ::_thesis: (f1 + f2) . c = r1 + r2 then A6: c in X /\ Y by XBOOLE_0:def_4; then A7: c in X by XBOOLE_0:def_4; A8: c in dom (f1 + f2) by A5, XBOOLE_0:def_4; then A9: c in (dom f1) /\ (dom f2) by VALUED_1:def_1; then c in dom f1 by XBOOLE_0:def_4; then A10: c in X /\ (dom f1) by A7, XBOOLE_0:def_4; A11: c in Y by A6, XBOOLE_0:def_4; c in dom f2 by A9, XBOOLE_0:def_4; then A12: c in Y /\ (dom f2) by A11, XBOOLE_0:def_4; thus (f1 + f2) . c = (f1 . c) + (f2 . c) by A8, VALUED_1:def_1 .= r1 + (f2 . c) by A3, A10 .= r1 + r2 by A4, A12 ; ::_thesis: verum end; hence (f1 + f2) | (X /\ Y) is constant by PARTFUN2:57; ::_thesis: ( (f1 - f2) | (X /\ Y) is constant & (f1 (#) f2) | (X /\ Y) is constant ) now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_-_f2))_holds_ (f1_-_f2)_._c_=_r1_-_r2 let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 - f2)) implies (f1 - f2) . c = r1 - r2 ) assume A13: c in (X /\ Y) /\ (dom (f1 - f2)) ; ::_thesis: (f1 - f2) . c = r1 - r2 then A14: c in X /\ Y by XBOOLE_0:def_4; then A15: c in X by XBOOLE_0:def_4; A16: c in dom (f1 - f2) by A13, XBOOLE_0:def_4; then A17: c in (dom f1) /\ (dom f2) by VALUED_1:12; then c in dom f1 by XBOOLE_0:def_4; then A18: c in X /\ (dom f1) by A15, XBOOLE_0:def_4; A19: c in Y by A14, XBOOLE_0:def_4; c in dom f2 by A17, XBOOLE_0:def_4; then A20: c in Y /\ (dom f2) by A19, XBOOLE_0:def_4; thus (f1 - f2) . c = (f1 . c) - (f2 . c) by A16, VALUED_1:13 .= r1 - (f2 . c) by A3, A18 .= r1 - r2 by A4, A20 ; ::_thesis: verum end; hence (f1 - f2) | (X /\ Y) is constant by PARTFUN2:57; ::_thesis: (f1 (#) f2) | (X /\ Y) is constant now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_(#)_f2))_holds_ (f1_(#)_f2)_._c_=_r1_*_r2 let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies (f1 (#) f2) . c = r1 * r2 ) assume A21: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; ::_thesis: (f1 (#) f2) . c = r1 * r2 then A22: c in X /\ Y by XBOOLE_0:def_4; c in dom (f1 (#) f2) by A21, XBOOLE_0:def_4; then A23: c in (dom f1) /\ (dom f2) by VALUED_1:def_4; then A24: c in dom f1 by XBOOLE_0:def_4; A25: c in dom f2 by A23, XBOOLE_0:def_4; c in Y by A22, XBOOLE_0:def_4; then A26: c in Y /\ (dom f2) by A25, XBOOLE_0:def_4; c in X by A22, XBOOLE_0:def_4; then A27: c in X /\ (dom f1) by A24, XBOOLE_0:def_4; thus (f1 (#) f2) . c = (f1 . c) * (f2 . c) by VALUED_1:5 .= r1 * (f2 . c) by A3, A27 .= r1 * r2 by A4, A26 ; ::_thesis: verum end; hence (f1 (#) f2) | (X /\ Y) is constant by PARTFUN2:57; ::_thesis: verum end; registration let C be non empty set ; let f be constant PartFunc of C,REAL; cluster - f -> constant ; coherence - f is constant proof consider r being Real such that A1: for c being Element of C st c in dom f holds f . c = r by PARTFUN2:def_1; now__::_thesis:_ex_p_being_Element_of_REAL_st_ for_c_being_Element_of_C_st_c_in_dom_(-_f)_holds_ (-_f)_._c_=_p take p = - r; ::_thesis: for c being Element of C st c in dom (- f) holds (- f) . c = p let c be Element of C; ::_thesis: ( c in dom (- f) implies (- f) . c = p ) assume c in dom (- f) ; ::_thesis: (- f) . c = p then c in dom f by VALUED_1:8; then - (f . c) = p by A1; hence (- f) . c = p by VALUED_1:8; ::_thesis: verum end; hence - f is constant by PARTFUN2:def_1; ::_thesis: verum end; cluster|.f.| -> constant ; coherence abs f is constant proof consider r being Real such that A2: for c being Element of C st c in dom f holds f . c = r by PARTFUN2:def_1; now__::_thesis:_ex_p_being_Element_of_REAL_st_ for_c_being_Element_of_C_st_c_in_dom_(abs_f)_holds_ (abs_f)_._c_=_p take p = abs r; ::_thesis: for c being Element of C st c in dom (abs f) holds (abs f) . c = p let c be Element of C; ::_thesis: ( c in dom (abs f) implies (abs f) . c = p ) assume c in dom (abs f) ; ::_thesis: (abs f) . c = p then c in dom f by VALUED_1:def_11; then abs (f . c) = p by A2; hence (abs f) . c = p by VALUED_1:18; ::_thesis: verum end; hence abs f is constant by PARTFUN2:def_1; ::_thesis: verum end; let p be real number ; clusterp (#) f -> constant ; coherence p (#) f is constant proof consider r being Real such that A3: for c being Element of C st c in dom f holds f . c = r by PARTFUN2:def_1; now__::_thesis:_ex_r1_being_Element_of_REAL_st_ for_c_being_Element_of_C_st_c_in_dom_(p_(#)_f)_holds_ (p_(#)_f)_._c_=_r1 take r1 = p * r; ::_thesis: for c being Element of C st c in dom (p (#) f) holds (p (#) f) . c = r1 let c be Element of C; ::_thesis: ( c in dom (p (#) f) implies (p (#) f) . c = r1 ) assume c in dom (p (#) f) ; ::_thesis: (p (#) f) . c = r1 then c in dom f by VALUED_1:def_5; then p * (f . c) = r1 by A3; hence (p (#) f) . c = r1 by VALUED_1:6; ::_thesis: verum end; hence p (#) f is constant by PARTFUN2:def_1; ::_thesis: verum end; end; theorem Th89: :: RFUNCT_1:89 for Y being set for C being non empty set for p being real number for f being PartFunc of C,REAL st f | Y is constant holds (p (#) f) | Y is constant proof let Y be set ; ::_thesis: for C being non empty set for p being real number for f being PartFunc of C,REAL st f | Y is constant holds (p (#) f) | Y is constant let C be non empty set ; ::_thesis: for p being real number for f being PartFunc of C,REAL st f | Y is constant holds (p (#) f) | Y is constant let p be real number ; ::_thesis: for f being PartFunc of C,REAL st f | Y is constant holds (p (#) f) | Y is constant let f be PartFunc of C,REAL; ::_thesis: ( f | Y is constant implies (p (#) f) | Y is constant ) (p (#) f) | Y = p (#) (f | Y) by Th49; hence ( f | Y is constant implies (p (#) f) | Y is constant ) ; ::_thesis: verum end; theorem Th90: :: RFUNCT_1:90 for Y being set for C being non empty set for f being PartFunc of C,REAL st f | Y is constant holds (- f) | Y is constant proof let Y be set ; ::_thesis: for C being non empty set for f being PartFunc of C,REAL st f | Y is constant holds (- f) | Y is constant let C be non empty set ; ::_thesis: for f being PartFunc of C,REAL st f | Y is constant holds (- f) | Y is constant let f be PartFunc of C,REAL; ::_thesis: ( f | Y is constant implies (- f) | Y is constant ) (- f) | Y = - (f | Y) by Th46; hence ( f | Y is constant implies (- f) | Y is constant ) ; ::_thesis: verum end; theorem Th91: :: RFUNCT_1:91 for Y being set for C being non empty set for f being PartFunc of C,REAL st f | Y is constant holds (abs f) | Y is constant proof let Y be set ; ::_thesis: for C being non empty set for f being PartFunc of C,REAL st f | Y is constant holds (abs f) | Y is constant let C be non empty set ; ::_thesis: for f being PartFunc of C,REAL st f | Y is constant holds (abs f) | Y is constant let f be PartFunc of C,REAL; ::_thesis: ( f | Y is constant implies (abs f) | Y is constant ) (abs f) | Y = abs (f | Y) by Th46; hence ( f | Y is constant implies (abs f) | Y is constant ) ; ::_thesis: verum end; theorem :: RFUNCT_1:92 for Y being set for C being non empty set for f being PartFunc of C,REAL st f | Y is constant holds ( ( for r being real number holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded ) proof let Y be set ; ::_thesis: for C being non empty set for f being PartFunc of C,REAL st f | Y is constant holds ( ( for r being real number holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded ) let C be non empty set ; ::_thesis: for f being PartFunc of C,REAL st f | Y is constant holds ( ( for r being real number holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded ) let f be PartFunc of C,REAL; ::_thesis: ( f | Y is constant implies ( ( for r being real number holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded ) ) assume A1: f | Y is constant ; ::_thesis: ( ( for r being real number holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & (abs f) | Y is bounded ) hereby ::_thesis: ( (- f) | Y is bounded & (abs f) | Y is bounded ) let r be real number ; ::_thesis: (r (#) f) | Y is bounded (r (#) f) | Y is constant by A1, Th89; hence (r (#) f) | Y is bounded ; ::_thesis: verum end; (- f) | Y is constant by A1, Th90; hence (- f) | Y is bounded ; ::_thesis: (abs f) | Y is bounded (abs f) | Y is constant by A1, Th91; hence (abs f) | Y is bounded ; ::_thesis: verum end; theorem :: RFUNCT_1:93 for X, Y being set for C being non empty set for f1, f2 being PartFunc of C,REAL holds ( ( f1 | X is bounded_above & f2 | Y is constant implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is constant implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies (f1 + f2) | (X /\ Y) is bounded ) ) by Th83; theorem :: RFUNCT_1:94 for X, Y being set for C being non empty set for f1, f2 being PartFunc of C,REAL holds ( ( f1 | X is bounded_above & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) ) ) proof let X, Y be set ; ::_thesis: for C being non empty set for f1, f2 being PartFunc of C,REAL holds ( ( f1 | X is bounded_above & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) ) ) let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,REAL holds ( ( f1 | X is bounded_above & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) ) ) let f1, f2 be PartFunc of C,REAL; ::_thesis: ( ( f1 | X is bounded_above & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) ) ) thus ( f1 | X is bounded_above & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_above ) ::_thesis: ( ( f1 | X is bounded_below & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) ) ) proof assume that A1: f1 | X is bounded_above and A2: f2 | Y is constant ; ::_thesis: (f1 - f2) | (X /\ Y) is bounded_above (- f2) | Y is constant by A2, Th90; hence (f1 - f2) | (X /\ Y) is bounded_above by A1, Th83; ::_thesis: verum end; thus ( f1 | X is bounded_below & f2 | Y is constant implies (f1 - f2) | (X /\ Y) is bounded_below ) ::_thesis: ( f1 | X is bounded & f2 | Y is constant implies ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) ) proof assume that A3: f1 | X is bounded_below and A4: f2 | Y is constant ; ::_thesis: (f1 - f2) | (X /\ Y) is bounded_below (- f2) | Y is constant by A4, Th90; hence (f1 - f2) | (X /\ Y) is bounded_below by A3, Th83; ::_thesis: verum end; assume that A5: f1 | X is bounded and A6: f2 | Y is constant ; ::_thesis: ( (f1 - f2) | (X /\ Y) is bounded & (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) (- f2) | Y is constant by A6, Th90; hence (f1 - f2) | (X /\ Y) is bounded by A5, Th83; ::_thesis: ( (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) thus (f2 - f1) | (X /\ Y) is bounded by A5, A6, Th84; ::_thesis: (f1 (#) f2) | (X /\ Y) is bounded thus (f1 (#) f2) | (X /\ Y) is bounded by A5, A6, Th84; ::_thesis: verum end;