:: CFUNCT_1 semantic presentation begin definition mode Complex is complex number ; end; definition let C be non empty set ; let f1, f2 be PartFunc of C,COMPLEX; deffunc H1( set ) -> Element of COMPLEX = (f1 /. \$1) * ((f2 /. \$1) "); funcf1 / f2 -> PartFunc of C,COMPLEX means :Def1: :: CFUNCT_1:def 1 ( dom it = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom it holds it /. c = (f1 /. c) * ((f2 /. c) ") ) ); existence ex b1 being PartFunc of C,COMPLEX st ( dom b1 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom b1 holds b1 /. c = (f1 /. c) * ((f2 /. c) ") ) ) proof defpred S1[ set ] means \$1 in (dom f1) /\ ((dom f2) \ (f2 " {0c})); consider F being PartFunc of C,COMPLEX such that A1: for c being Element of C holds ( c in dom F iff S1[c] ) and A2: for c being Element of C st c in dom F holds F /. c = H1(c) from PARTFUN2:sch_2(); take F ; ::_thesis: ( dom F = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom F holds F /. c = (f1 /. c) * ((f2 /. c) ") ) ) thus dom F = (dom f1) /\ ((dom f2) \ (f2 " {0})) by A1, SUBSET_1:3; ::_thesis: for c being Element of C st c in dom F holds F /. c = (f1 /. c) * ((f2 /. c) ") thus for c being Element of C st c in dom F holds F /. c = (f1 /. c) * ((f2 /. c) ") by A2; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,COMPLEX st dom b1 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom b1 holds b1 /. c = (f1 /. c) * ((f2 /. c) ") ) & dom b2 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom b2 holds b2 /. c = (f1 /. c) * ((f2 /. c) ") ) holds b1 = b2 proof set X = (dom f1) /\ ((dom f2) \ (f2 " {0})); thus for f, g being PartFunc of C,COMPLEX st dom f = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom f holds f /. c = H1(c) ) & dom g = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom g holds g /. c = H1(c) ) holds f = g from PARTFUN2:sch_3(); ::_thesis: verum end; end; :: deftheorem Def1 defines / CFUNCT_1:def_1_:_ for C being non empty set for f1, f2, b4 being PartFunc of C,COMPLEX holds ( b4 = f1 / f2 iff ( dom b4 = (dom f1) /\ ((dom f2) \ (f2 " {0})) & ( for c being Element of C st c in dom b4 holds b4 /. c = (f1 /. c) * ((f2 /. c) ") ) ) ); definition let C be non empty set ; let f be PartFunc of C,COMPLEX; deffunc H1( set ) -> Element of COMPLEX = (f /. \$1) " ; funcf ^ -> PartFunc of C,COMPLEX means :Def2: :: CFUNCT_1:def 2 ( dom it = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom it holds it /. c = (f /. c) " ) ); existence ex b1 being PartFunc of C,COMPLEX st ( dom b1 = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom b1 holds b1 /. c = (f /. c) " ) ) proof defpred S1[ set ] means \$1 in (dom f) \ (f " {0c}); consider F being PartFunc of C,COMPLEX such that A1: for c being Element of C holds ( c in dom F iff S1[c] ) and A2: for c being Element of C st c in dom F holds F /. c = H1(c) from PARTFUN2:sch_2(); take F ; ::_thesis: ( dom F = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom F holds F /. c = (f /. c) " ) ) thus dom F = (dom f) \ (f " {0}) by A1, SUBSET_1:3; ::_thesis: for c being Element of C st c in dom F holds F /. c = (f /. c) " let c be Element of C; ::_thesis: ( c in dom F implies F /. c = (f /. c) " ) assume c in dom F ; ::_thesis: F /. c = (f /. c) " hence F /. c = (f /. c) " by A2; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,COMPLEX st dom b1 = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom b1 holds b1 /. c = (f /. c) " ) & dom b2 = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom b2 holds b2 /. c = (f /. c) " ) holds b1 = b2 proof set X = (dom f) \ (f " {0}); thus for f, g being PartFunc of C,COMPLEX st dom f = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom f holds f /. c = H1(c) ) & dom g = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom g holds g /. c = H1(c) ) holds f = g from PARTFUN2:sch_3(); ::_thesis: verum end; end; :: deftheorem Def2 defines ^ CFUNCT_1:def_2_:_ for C being non empty set for f, b3 being PartFunc of C,COMPLEX holds ( b3 = f ^ iff ( dom b3 = (dom f) \ (f " {0}) & ( for c being Element of C st c in dom b3 holds b3 /. c = (f /. c) " ) ) ); theorem Th1: :: CFUNCT_1:1 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX holds ( dom (f1 + f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 + f2) holds (f1 + f2) /. c = (f1 /. c) + (f2 /. c) ) ) proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds ( dom (f1 + f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 + f2) holds (f1 + f2) /. c = (f1 /. c) + (f2 /. c) ) ) let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( dom (f1 + f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 + f2) holds (f1 + f2) /. c = (f1 /. c) + (f2 /. c) ) ) thus A1: dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def_1; ::_thesis: for c being Element of C st c in dom (f1 + f2) holds (f1 + f2) /. c = (f1 /. c) + (f2 /. c) now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_+_f2)_holds_ (f1_+_f2)_/._c_=_(f1_/._c)_+_(f2_/._c) let c be Element of C; ::_thesis: ( c in dom (f1 + f2) implies (f1 + f2) /. c = (f1 /. c) + (f2 /. c) ) assume A2: c in dom (f1 + f2) ; ::_thesis: (f1 + f2) /. c = (f1 /. c) + (f2 /. c) then c in dom f1 by A1, XBOOLE_0:def_4; then A3: f1 . c = f1 /. c by PARTFUN1:def_6; c in dom f2 by A1, A2, XBOOLE_0:def_4; then A4: f2 . c = f2 /. c by PARTFUN1:def_6; thus (f1 + f2) /. c = (f1 + f2) . c by A2, PARTFUN1:def_6 .= (f1 /. c) + (f2 /. c) by A2, A3, A4, VALUED_1:def_1 ; ::_thesis: verum end; hence for c being Element of C st c in dom (f1 + f2) holds (f1 + f2) /. c = (f1 /. c) + (f2 /. c) ; ::_thesis: verum end; theorem Th2: :: CFUNCT_1:2 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX holds ( dom (f1 - f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 - f2) holds (f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) ) proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds ( dom (f1 - f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 - f2) holds (f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) ) let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( dom (f1 - f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 - f2) holds (f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) ) A1: dom (f1 - f2) = (dom f1) /\ (dom (- f2)) by VALUED_1:def_1; hence dom (f1 - f2) = (dom f1) /\ (dom f2) by VALUED_1:8; ::_thesis: for c being Element of C st c in dom (f1 - f2) holds (f1 - f2) /. c = (f1 /. c) - (f2 /. c) now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_f2)_holds_ (f1_-_f2)_/._c_=_(f1_/._c)_-_(f2_/._c) let c be Element of C; ::_thesis: ( c in dom (f1 - f2) implies (f1 - f2) /. c = (f1 /. c) - (f2 /. c) ) assume A2: c in dom (f1 - f2) ; ::_thesis: (f1 - f2) /. c = (f1 /. c) - (f2 /. c) then A3: ( dom (- f2) = dom f2 & c in dom (- f2) ) by A1, VALUED_1:8, XBOOLE_0:def_4; c in dom f1 by A1, A2, XBOOLE_0:def_4; then A4: f1 /. c = f1 . c by PARTFUN1:def_6; thus (f1 - f2) /. c = (f1 - f2) . c by A2, PARTFUN1:def_6 .= (f1 . c) - (f2 . c) by A2, VALUED_1:13 .= (f1 /. c) - (f2 /. c) by A3, A4, PARTFUN1:def_6 ; ::_thesis: verum end; hence for c being Element of C st c in dom (f1 - f2) holds (f1 - f2) /. c = (f1 /. c) - (f2 /. c) ; ::_thesis: verum end; theorem Th3: :: CFUNCT_1:3 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX holds ( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 (#) f2) holds (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ) ) proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds ( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 (#) f2) holds (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ) ) let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 (#) f2) holds (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ) ) thus A1: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def_4; ::_thesis: for c being Element of C st c in dom (f1 (#) f2) holds (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_(#)_f2)_holds_ (f1_(#)_f2)_/._c_=_(f1_/._c)_*_(f2_/._c) let c be Element of C; ::_thesis: ( c in dom (f1 (#) f2) implies (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ) assume A2: c in dom (f1 (#) f2) ; ::_thesis: (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) then c in dom f1 by A1, XBOOLE_0:def_4; then A3: f1 . c = f1 /. c by PARTFUN1:def_6; c in dom f2 by A1, A2, XBOOLE_0:def_4; then A4: f2 . c = f2 /. c by PARTFUN1:def_6; thus (f1 (#) f2) /. c = (f1 (#) f2) . c by A2, PARTFUN1:def_6 .= (f1 /. c) * (f2 /. c) by A2, A3, A4, VALUED_1:def_4 ; ::_thesis: verum end; hence for c being Element of C st c in dom (f1 (#) f2) holds (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ; ::_thesis: verum end; theorem Th4: :: CFUNCT_1:4 for C being non empty set for f being PartFunc of C,COMPLEX for r being Element of COMPLEX holds ( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds (r (#) f) /. c = r * (f /. c) ) ) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX for r being Element of COMPLEX holds ( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds (r (#) f) /. c = r * (f /. c) ) ) let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds ( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds (r (#) f) /. c = r * (f /. c) ) ) let r be Element of COMPLEX ; ::_thesis: ( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds (r (#) f) /. c = r * (f /. c) ) ) thus A1: dom (r (#) f) = dom f by VALUED_1:def_5; ::_thesis: for c being Element of C st c in dom (r (#) f) holds (r (#) f) /. c = r * (f /. c) now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_f)_holds_ (r_(#)_f)_/._c_=_r_*_(f_/._c) let c be Element of C; ::_thesis: ( c in dom (r (#) f) implies (r (#) f) /. c = r * (f /. c) ) assume A2: c in dom (r (#) f) ; ::_thesis: (r (#) f) /. c = r * (f /. c) hence (r (#) f) /. c = (r (#) f) . c by PARTFUN1:def_6 .= r * (f . c) by VALUED_1:6 .= r * (f /. c) by A1, A2, PARTFUN1:def_6 ; ::_thesis: verum end; hence for c being Element of C st c in dom (r (#) f) holds (r (#) f) /. c = r * (f /. c) ; ::_thesis: verum end; theorem Th5: :: CFUNCT_1:5 for C being non empty set for f being PartFunc of C,COMPLEX holds ( dom (- f) = dom f & ( for c being Element of C st c in dom (- f) holds (- f) /. c = - (f /. c) ) ) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds ( dom (- f) = dom f & ( for c being Element of C st c in dom (- f) holds (- f) /. c = - (f /. c) ) ) let f be PartFunc of C,COMPLEX; ::_thesis: ( dom (- f) = dom f & ( for c being Element of C st c in dom (- f) holds (- f) /. c = - (f /. c) ) ) thus A1: dom (- f) = dom f by VALUED_1:8; ::_thesis: for c being Element of C st c in dom (- f) holds (- f) /. c = - (f /. c) now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(-_f)_holds_ (-_f)_/._c_=_-_(f_/._c) let c be Element of C; ::_thesis: ( c in dom (- f) implies (- f) /. c = - (f /. c) ) assume A2: c in dom (- f) ; ::_thesis: (- f) /. c = - (f /. c) hence (- f) /. c = (- f) . c by PARTFUN1:def_6 .= - (f . c) by VALUED_1:8 .= - (f /. c) by A1, A2, PARTFUN1:def_6 ; ::_thesis: verum end; hence for c being Element of C st c in dom (- f) holds (- f) /. c = - (f /. c) ; ::_thesis: verum end; Lm1: for x, Y being set for C being non empty set for f being PartFunc of C,COMPLEX holds ( x in f " Y iff ( x in dom f & f /. x in Y ) ) by PARTFUN2:26; theorem Th6: :: CFUNCT_1:6 for C being non empty set for g being PartFunc of C,COMPLEX holds ( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) ) proof let C be non empty set ; ::_thesis: for g being PartFunc of C,COMPLEX holds ( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) ) let g be PartFunc of C,COMPLEX; ::_thesis: ( dom (g ^) c= dom g & (dom g) /\ ((dom g) \ (g " {0})) = (dom g) \ (g " {0}) ) dom (g ^) = (dom g) \ (g " {0c}) by Def2; hence dom (g ^) c= dom g by XBOOLE_1:36; ::_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, XBOOLE_1:36; ::_thesis: verum end; theorem Th7: :: CFUNCT_1:7 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) = ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) let f1, f2 be PartFunc of C,COMPLEX; ::_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 A2: x in dom (f1 (#) f2) by XBOOLE_0:def_5; reconsider x1 = x as Element of C by A1; not x in (f1 (#) f2) " {0c} by A1, XBOOLE_0:def_5; then not (f1 (#) f2) /. x1 in {0c} by A2, PARTFUN2:26; then (f1 (#) f2) /. x1 <> 0c by TARSKI:def_1; then A3: (f1 /. x1) * (f2 /. x1) <> 0c by A2, Th3; then f2 /. x1 <> 0c ; then not f2 /. x1 in {0c} by TARSKI:def_1; then A4: not x1 in f2 " {0c} by PARTFUN2:26; A5: x1 in (dom f1) /\ (dom f2) by A2, Th3; then x1 in dom f2 by XBOOLE_0:def_4; then A6: x in (dom f2) \ (f2 " {0c}) by A4, XBOOLE_0:def_5; f1 /. x1 <> 0c by A3; then not f1 /. x1 in {0c} by TARSKI:def_1; then A7: not x1 in f1 " {0c} by PARTFUN2:26; x1 in dom f1 by A5, XBOOLE_0:def_4; then x in (dom f1) \ (f1 " {0c}) by A7, XBOOLE_0:def_5; hence x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) by A6, 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 A8: x in ((dom f1) \ (f1 " {0})) /\ ((dom f2) \ (f2 " {0})) ; ::_thesis: x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) then reconsider x1 = x as Element of C ; A9: x in (dom f2) \ (f2 " {0c}) by A8, XBOOLE_0:def_4; then A10: x in dom f2 by XBOOLE_0:def_5; not x in f2 " {0c} by A9, XBOOLE_0:def_5; then not f2 /. x1 in {0c} by A10, PARTFUN2:26; then A11: f2 /. x1 <> 0c by TARSKI:def_1; A12: x in (dom f1) \ (f1 " {0c}) by A8, XBOOLE_0:def_4; then A13: x in dom f1 by XBOOLE_0:def_5; then x1 in (dom f1) /\ (dom f2) by A10, XBOOLE_0:def_4; then A14: x1 in dom (f1 (#) f2) by Th3; not x in f1 " {0c} by A12, XBOOLE_0:def_5; then not f1 /. x1 in {0c} by A13, PARTFUN2:26; then f1 /. x1 <> 0c by TARSKI:def_1; then (f1 /. x1) * (f2 /. x1) <> 0c by A11, XCMPLX_1:6; then (f1 (#) f2) /. x1 <> 0c by A14, Th3; then not (f1 (#) f2) /. x1 in {0c} by TARSKI:def_1; then not x in (f1 (#) f2) " {0c} by PARTFUN2:26; hence x in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0}) by A14, XBOOLE_0:def_5; ::_thesis: verum end; end; theorem Th8: :: CFUNCT_1:8 for C being non empty set for c being Element of C for f being PartFunc of C,COMPLEX 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 PartFunc of C,COMPLEX st c in dom (f ^) holds f /. c <> 0 let c be Element of C; ::_thesis: for f being PartFunc of C,COMPLEX st c in dom (f ^) holds f /. c <> 0 let f be PartFunc of C,COMPLEX; ::_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 " {0c}) by A1, Def2; then A4: not c in f " {0c} by XBOOLE_0:def_5; now__::_thesis:_contradiction percases ( not c in dom f or not f /. c in {0c} ) by A4, PARTFUN2:26; suppose not c in dom f ; ::_thesis: contradiction hence contradiction by A3, XBOOLE_0:def_5; ::_thesis: verum end; suppose not f /. c in {0c} ; ::_thesis: contradiction hence contradiction by A2, TARSKI:def_1; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem Th9: :: CFUNCT_1:9 for C being non empty set for f being PartFunc of C,COMPLEX holds (f ^) " {0} = {} proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds (f ^) " {0} = {} let f be PartFunc of C,COMPLEX; ::_thesis: (f ^) " {0} = {} set x = the Element of (f ^) " {0c}; assume A1: (f ^) " {0} <> {} ; ::_thesis: contradiction then A2: the Element of (f ^) " {0c} in dom (f ^) by Lm1; A3: (f ^) /. the Element of (f ^) " {0c} in {0c} by A1, Lm1; reconsider x = the Element of (f ^) " {0c} as Element of C by A2; x in (dom f) \ (f " {0c}) by A2, Def2; then ( x in dom f & not x in f " {0c} ) by XBOOLE_0:def_5; then A4: not f /. x in {0c} by PARTFUN2:26; (f ^) /. x = 0c by A3, TARSKI:def_1; then (f /. x) " = 0c by A2, Def2; hence contradiction by A4, TARSKI:def_1, XCMPLX_1:202; ::_thesis: verum end; theorem Th10: :: CFUNCT_1:10 for C being non empty set for f being PartFunc of C,COMPLEX holds ( |.f.| " {0} = f " {0} & (- f) " {0} = f " {0} ) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds ( |.f.| " {0} = f " {0} & (- f) " {0} = f " {0} ) let f be PartFunc of C,COMPLEX; ::_thesis: ( |.f.| " {0} = f " {0} & (- f) " {0} = f " {0} ) A1: dom |.f.| = dom f by VALUED_1:def_11; now__::_thesis:_for_c_being_Element_of_C_holds_ (_(_c_in_|.f.|_"_{0}_implies_c_in_f_"_{0c}_)_&_(_c_in_f_"_{0c}_implies_c_in_|.f.|_"_{0}_)_) let c be Element of C; ::_thesis: ( ( c in |.f.| " {0} implies c in f " {0c} ) & ( c in f " {0c} implies c in |.f.| " {0} ) ) thus ( c in |.f.| " {0} implies c in f " {0c} ) ::_thesis: ( c in f " {0c} implies c in |.f.| " {0} ) proof assume A2: c in |.f.| " {0} ; ::_thesis: c in f " {0c} then c in dom |.f.| by FUNCT_1:def_7; then A3: c in dom f by VALUED_1:def_11; |.f.| . c in {0} by A2, FUNCT_1:def_7; then |.f.| . c = 0 by TARSKI:def_1; then A4: |.(f . c).| = 0 by VALUED_1:18; c in dom |.f.| by A2, FUNCT_1:def_7; then f . c = f /. c by A1, PARTFUN1:def_6; then f /. c = 0c by A4, COMPLEX1:45; then f /. c in {0c} by TARSKI:def_1; hence c in f " {0c} by A3, PARTFUN2:26; ::_thesis: verum end; assume A5: c in f " {0c} ; ::_thesis: c in |.f.| " {0} then f /. c in {0c} by PARTFUN2:26; then A6: |.(f /. c).| = 0 by COMPLEX1:44, TARSKI:def_1; A7: c in dom f by A5, PARTFUN2:26; then f . c = f /. c by PARTFUN1:def_6; then |.f.| . c = 0 by A6, VALUED_1:18; then A8: |.f.| . c in {0} by TARSKI:def_1; c in dom |.f.| by A7, VALUED_1:def_11; hence c in |.f.| " {0} by A8, FUNCT_1:def_7; ::_thesis: verum end; hence |.f.| " {0} = f " {0} by SUBSET_1:3; ::_thesis: (- f) " {0} = f " {0} now__::_thesis:_for_c_being_Element_of_C_holds_ (_(_c_in_(-_f)_"_{0c}_implies_c_in_f_"_{0c}_)_&_(_c_in_f_"_{0c}_implies_c_in_(-_f)_"_{0c}_)_) let c be Element of C; ::_thesis: ( ( c in (- f) " {0c} implies c in f " {0c} ) & ( c in f " {0c} implies c in (- f) " {0c} ) ) thus ( c in (- f) " {0c} implies c in f " {0c} ) ::_thesis: ( c in f " {0c} implies c in (- f) " {0c} ) proof assume A9: c in (- f) " {0c} ; ::_thesis: c in f " {0c} then A10: c in dom (- f) by PARTFUN2:26; (- f) /. c in {0c} by A9, PARTFUN2:26; then (- f) /. c = 0c by TARSKI:def_1; then - (- (f /. c)) = - 0c by A10, Th5; then A11: f /. c in {0c} by TARSKI:def_1; c in dom f by A10, Th5; hence c in f " {0c} by A11, PARTFUN2:26; ::_thesis: verum end; assume A12: c in f " {0c} ; ::_thesis: c in (- f) " {0c} then f /. c in {0c} by PARTFUN2:26; then A13: f /. c = 0c by TARSKI:def_1; A14: c in dom f by A12, PARTFUN2:26; then c in dom (- f) by Th5; then (- f) /. c = - 0c by A13, Th5; then A15: (- f) /. c in {0c} by TARSKI:def_1; c in dom (- f) by A14, Th5; hence c in (- f) " {0c} by A15, PARTFUN2:26; ::_thesis: verum end; hence (- f) " {0} = f " {0} by SUBSET_1:3; ::_thesis: verum end; theorem Th11: :: CFUNCT_1:11 for C being non empty set for f being PartFunc of C,COMPLEX holds dom ((f ^) ^) = dom (f | (dom (f ^))) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds dom ((f ^) ^) = dom (f | (dom (f ^))) let f be PartFunc of C,COMPLEX; ::_thesis: dom ((f ^) ^) = dom (f | (dom (f ^))) A1: dom (f ^) = (dom f) \ (f " {0c}) by Def2; thus dom ((f ^) ^) = (dom (f ^)) \ ((f ^) " {0c}) by Def2 .= (dom (f ^)) \ {} by Th9 .= (dom f) /\ (dom (f ^)) by A1, XBOOLE_1:28, XBOOLE_1:36 .= dom (f | (dom (f ^))) by RELAT_1:61 ; ::_thesis: verum end; theorem Th12: :: CFUNCT_1:12 for C being non empty set for f being PartFunc of C,COMPLEX for r being Element of COMPLEX st r <> 0 holds (r (#) f) " {0} = f " {0} proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX for r being Element of COMPLEX st r <> 0 holds (r (#) f) " {0} = f " {0} let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX st r <> 0 holds (r (#) f) " {0} = f " {0} let r be Element of COMPLEX ; ::_thesis: ( r <> 0 implies (r (#) f) " {0} = f " {0} ) assume A1: r <> 0 ; ::_thesis: (r (#) f) " {0} = f " {0} now__::_thesis:_for_c_being_Element_of_C_holds_ (_(_c_in_(r_(#)_f)_"_{0c}_implies_c_in_f_"_{0c}_)_&_(_c_in_f_"_{0c}_implies_c_in_(r_(#)_f)_"_{0c}_)_) let c be Element of C; ::_thesis: ( ( c in (r (#) f) " {0c} implies c in f " {0c} ) & ( c in f " {0c} implies c in (r (#) f) " {0c} ) ) thus ( c in (r (#) f) " {0c} implies c in f " {0c} ) ::_thesis: ( c in f " {0c} implies c in (r (#) f) " {0c} ) proof assume A2: c in (r (#) f) " {0c} ; ::_thesis: c in f " {0c} then A3: c in dom (r (#) f) by PARTFUN2:26; (r (#) f) /. c in {0c} by A2, PARTFUN2:26; then (r (#) f) /. c = 0c by TARSKI:def_1; then r * (f /. c) = 0c by A3, Th4; then f /. c = 0c by A1, XCMPLX_1:6; then A4: f /. c in {0c} by TARSKI:def_1; c in dom f by A3, Th4; hence c in f " {0c} by A4, PARTFUN2:26; ::_thesis: verum end; assume A5: c in f " {0c} ; ::_thesis: c in (r (#) f) " {0c} then f /. c in {0c} by PARTFUN2:26; then f /. c = 0c by TARSKI:def_1; then A6: r * (f /. c) = 0c ; A7: c in dom f by A5, PARTFUN2:26; then c in dom (r (#) f) by Th4; then (r (#) f) /. c = 0c by A6, Th4; then A8: (r (#) f) /. c in {0c} by TARSKI:def_1; c in dom (r (#) f) by A7, Th4; hence c in (r (#) f) " {0c} by A8, PARTFUN2:26; ::_thesis: verum end; hence (r (#) f) " {0} = f " {0} by SUBSET_1:3; ::_thesis: verum end; begin theorem :: CFUNCT_1:13 for C being non empty set for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 + f2) + f3 = f1 + (f2 + f3) proof let C be non empty set ; ::_thesis: for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 + f2) + f3 = f1 + (f2 + f3) let f1, f2, f3 be PartFunc of C,COMPLEX; ::_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_Element_of_C_st_c_in_dom_((f1_+_f2)_+_f3)_holds_ ((f1_+_f2)_+_f3)_/._c_=_(f1_+_(f2_+_f3))_/._c let c be Element of C; ::_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, Th1 .= ((f1 /. c) + (f2 /. c)) + (f3 /. c) by A3, Th1 .= (f1 /. c) + ((f2 /. c) + (f3 /. c)) .= (f1 /. c) + ((f2 + f3) /. c) by A4, Th1 .= (f1 + (f2 + f3)) /. c by A1, A2, Th1 ; ::_thesis: verum end; hence (f1 + f2) + f3 = f1 + (f2 + f3) by A1, PARTFUN2:1; ::_thesis: verum end; theorem Th14: :: CFUNCT_1:14 for C being non empty set for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) proof let C be non empty set ; ::_thesis: for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) let f1, f2, f3 be PartFunc of C,COMPLEX; ::_thesis: (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) A1: dom ((f1 (#) f2) (#) f3) = (dom (f1 (#) f2)) /\ (dom f3) by Th3 .= ((dom f1) /\ (dom f2)) /\ (dom f3) by Th3 .= (dom f1) /\ ((dom f2) /\ (dom f3)) by XBOOLE_1:16 .= (dom f1) /\ (dom (f2 (#) f3)) by Th3 .= dom (f1 (#) (f2 (#) f3)) by Th3 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_(#)_f3)_holds_ ((f1_(#)_f2)_(#)_f3)_/._c_=_(f1_(#)_(f2_(#)_f3))_/._c let c be Element of C; ::_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 Th3; then A3: c in dom (f1 (#) f2) by XBOOLE_0:def_4; c in (dom f1) /\ (dom (f2 (#) f3)) by A1, A2, Th3; then A4: c in dom (f2 (#) f3) by XBOOLE_0:def_4; thus ((f1 (#) f2) (#) f3) /. c = ((f1 (#) f2) /. c) * (f3 /. c) by A2, Th3 .= ((f1 /. c) * (f2 /. c)) * (f3 /. c) by A3, Th3 .= (f1 /. c) * ((f2 /. c) * (f3 /. c)) .= (f1 /. c) * ((f2 (#) f3) /. c) by A4, Th3 .= (f1 (#) (f2 (#) f3)) /. c by A1, A2, Th3 ; ::_thesis: verum end; hence (f1 (#) f2) (#) f3 = f1 (#) (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum end; theorem Th15: :: CFUNCT_1:15 for C being non empty set for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) proof let C be non empty set ; ::_thesis: for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) let f1, f2, f3 be PartFunc of C,COMPLEX; ::_thesis: (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) A1: dom ((f1 + f2) (#) f3) = (dom (f1 + f2)) /\ (dom f3) by Th3 .= ((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 Th3 .= (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by Th3 .= dom ((f1 (#) f3) + (f2 (#) f3)) by VALUED_1:def_1 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_(#)_f3)_holds_ ((f1_+_f2)_(#)_f3)_/._c_=_((f1_(#)_f3)_+_(f2_(#)_f3))_/._c let c be Element of C; ::_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 A3: c in (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by A1, VALUED_1:def_1; then A4: c in dom (f1 (#) f3) by XBOOLE_0:def_4; c in (dom (f1 + f2)) /\ (dom f3) by A2, Th3; then A5: c in dom (f1 + f2) by XBOOLE_0:def_4; A6: c in dom (f2 (#) f3) by A3, XBOOLE_0:def_4; thus ((f1 + f2) (#) f3) /. c = ((f1 + f2) /. c) * (f3 /. c) by A2, Th3 .= ((f1 /. c) + (f2 /. c)) * (f3 /. c) by A5, Th1 .= ((f1 /. c) * (f3 /. c)) + ((f2 /. c) * (f3 /. c)) .= ((f1 (#) f3) /. c) + ((f2 /. c) * (f3 /. c)) by A4, Th3 .= ((f1 (#) f3) /. c) + ((f2 (#) f3) /. c) by A6, Th3 .= ((f1 (#) f3) + (f2 (#) f3)) /. c by A1, A2, Th1 ; ::_thesis: verum end; hence (f1 + f2) (#) f3 = (f1 (#) f3) + (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: CFUNCT_1:16 for C being non empty set for f3, f1, f2 being PartFunc of C,COMPLEX holds f3 (#) (f1 + f2) = (f3 (#) f1) + (f3 (#) f2) by Th15; theorem Th17: :: CFUNCT_1:17 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX for r being Element of COMPLEX holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2 proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX for r being Element of COMPLEX holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2 let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds r (#) (f1 (#) f2) = (r (#) f1) (#) f2 let r be Element of COMPLEX ; ::_thesis: r (#) (f1 (#) f2) = (r (#) f1) (#) f2 A1: dom (r (#) (f1 (#) f2)) = dom (f1 (#) f2) by Th4 .= (dom f1) /\ (dom f2) by Th3 .= (dom (r (#) f1)) /\ (dom f2) by Th4 .= dom ((r (#) f1) (#) f2) by Th3 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_(#)_f2))_holds_ (r_(#)_(f1_(#)_f2))_/._c_=_((r_(#)_f1)_(#)_f2)_/._c let c be Element of C; ::_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 A3: c in dom (f1 (#) f2) by Th4; c in (dom (r (#) f1)) /\ (dom f2) by A1, A2, Th3; then A4: c in dom (r (#) f1) by XBOOLE_0:def_4; thus (r (#) (f1 (#) f2)) /. c = r * ((f1 (#) f2) /. c) by A2, Th4 .= r * ((f1 /. c) * (f2 /. c)) by A3, Th3 .= (r * (f1 /. c)) * (f2 /. c) .= ((r (#) f1) /. c) * (f2 /. c) by A4, Th4 .= ((r (#) f1) (#) f2) /. c by A1, A2, Th3 ; ::_thesis: verum end; hence r (#) (f1 (#) f2) = (r (#) f1) (#) f2 by A1, PARTFUN2:1; ::_thesis: verum end; theorem Th18: :: CFUNCT_1:18 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX for r being Element of COMPLEX holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2) proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX for r being Element of COMPLEX holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2) let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds r (#) (f1 (#) f2) = f1 (#) (r (#) f2) let r be Element of COMPLEX ; ::_thesis: r (#) (f1 (#) f2) = f1 (#) (r (#) f2) A1: dom (r (#) (f1 (#) f2)) = dom (f1 (#) f2) by Th4 .= (dom f1) /\ (dom f2) by Th3 .= (dom f1) /\ (dom (r (#) f2)) by Th4 .= dom (f1 (#) (r (#) f2)) by Th3 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_(#)_f2))_holds_ (r_(#)_(f1_(#)_f2))_/._c_=_(f1_(#)_(r_(#)_f2))_/._c let c be Element of C; ::_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 A3: c in dom (f1 (#) f2) by Th4; c in (dom f1) /\ (dom (r (#) f2)) by A1, A2, Th3; then A4: c in dom (r (#) f2) by XBOOLE_0:def_4; thus (r (#) (f1 (#) f2)) /. c = r * ((f1 (#) f2) /. c) by A2, Th4 .= r * ((f1 /. c) * (f2 /. c)) by A3, Th3 .= (f1 /. c) * (r * (f2 /. c)) .= (f1 /. c) * ((r (#) f2) /. c) by A4, Th4 .= (f1 (#) (r (#) f2)) /. c by A1, A2, Th3 ; ::_thesis: verum end; hence r (#) (f1 (#) f2) = f1 (#) (r (#) f2) by A1, PARTFUN2:1; ::_thesis: verum end; theorem Th19: :: CFUNCT_1:19 for C being non empty set for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) proof let C be non empty set ; ::_thesis: for f1, f2, f3 being PartFunc of C,COMPLEX holds (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) let f1, f2, f3 be PartFunc of C,COMPLEX; ::_thesis: (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) A1: dom ((f1 - f2) (#) f3) = (dom (f1 - f2)) /\ (dom f3) by Th3 .= ((dom f1) /\ (dom f2)) /\ ((dom f3) /\ (dom f3)) by Th2 .= (((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 Th3 .= (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by Th3 .= dom ((f1 (#) f3) - (f2 (#) f3)) by Th2 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_-_f2)_(#)_f3)_holds_ ((f1_-_f2)_(#)_f3)_/._c_=_((f1_(#)_f3)_-_(f2_(#)_f3))_/._c let c be Element of C; ::_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 Th3; then A3: c in dom (f1 - f2) by XBOOLE_0:def_4; A4: c in (dom (f1 (#) f3)) /\ (dom (f2 (#) f3)) by A1, A2, Th2; then A5: c in dom (f1 (#) f3) by XBOOLE_0:def_4; A6: c in dom (f2 (#) f3) by A4, XBOOLE_0:def_4; thus ((f1 - f2) (#) f3) /. c = ((f1 - f2) /. c) * (f3 /. c) by A2, Th3 .= ((f1 /. c) - (f2 /. c)) * (f3 /. c) by A3, Th2 .= ((f1 /. c) * (f3 /. c)) - ((f2 /. c) * (f3 /. c)) .= ((f1 (#) f3) /. c) - ((f2 /. c) * (f3 /. c)) by A5, Th3 .= ((f1 (#) f3) /. c) - ((f2 (#) f3) /. c) by A6, Th3 .= ((f1 (#) f3) - (f2 (#) f3)) /. c by A1, A2, Th2 ; ::_thesis: verum end; hence (f1 - f2) (#) f3 = (f1 (#) f3) - (f2 (#) f3) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: CFUNCT_1:20 for C being non empty set for f3, f1, f2 being PartFunc of C,COMPLEX holds (f3 (#) f1) - (f3 (#) f2) = f3 (#) (f1 - f2) by Th19; theorem :: CFUNCT_1:21 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX for r being Element of COMPLEX holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX for r being Element of COMPLEX holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) let r be Element of COMPLEX ; ::_thesis: r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) A1: dom (r (#) (f1 + f2)) = dom (f1 + f2) by Th4 .= (dom f1) /\ (dom f2) by VALUED_1:def_1 .= (dom f1) /\ (dom (r (#) f2)) by Th4 .= (dom (r (#) f1)) /\ (dom (r (#) f2)) by Th4 .= dom ((r (#) f1) + (r (#) f2)) by VALUED_1:def_1 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_+_f2))_holds_ (r_(#)_(f1_+_f2))_/._c_=_((r_(#)_f1)_+_(r_(#)_f2))_/._c let c be Element of C; ::_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 Th4; 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, Th4 .= r * ((f1 /. c) + (f2 /. c)) by A3, Th1 .= (r * (f1 /. c)) + (r * (f2 /. c)) .= ((r (#) f1) /. c) + (r * (f2 /. c)) by A5, Th4 .= ((r (#) f1) /. c) + ((r (#) f2) /. c) by A6, Th4 .= ((r (#) f1) + (r (#) f2)) /. c by A1, A2, Th1 ; ::_thesis: verum end; hence r (#) (f1 + f2) = (r (#) f1) + (r (#) f2) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: CFUNCT_1:22 for C being non empty set for f being PartFunc of C,COMPLEX for r, q being Element of COMPLEX holds (r * q) (#) f = r (#) (q (#) f) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX for r, q being Element of COMPLEX holds (r * q) (#) f = r (#) (q (#) f) let f be PartFunc of C,COMPLEX; ::_thesis: for r, q being Element of COMPLEX holds (r * q) (#) f = r (#) (q (#) f) let r, q be Element of COMPLEX ; ::_thesis: (r * q) (#) f = r (#) (q (#) f) A1: dom ((r * q) (#) f) = dom f by Th4 .= dom (q (#) f) by Th4 .= dom (r (#) (q (#) f)) by Th4 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((r_*_q)_(#)_f)_holds_ ((r_*_q)_(#)_f)_/._c_=_(r_(#)_(q_(#)_f))_/._c let c be Element of C; ::_thesis: ( c in dom ((r * q) (#) f) implies ((r * q) (#) f) /. c = (r (#) (q (#) f)) /. c ) assume A2: c in dom ((r * q) (#) f) ; ::_thesis: ((r * q) (#) f) /. c = (r (#) (q (#) f)) /. c then A3: c in dom (q (#) f) by A1, Th4; thus ((r * q) (#) f) /. c = (r * q) * (f /. c) by A2, Th4 .= r * (q * (f /. c)) .= r * ((q (#) f) /. c) by A3, Th4 .= (r (#) (q (#) f)) /. c by A1, A2, Th4 ; ::_thesis: verum end; hence (r * q) (#) f = r (#) (q (#) f) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: CFUNCT_1:23 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX for r being Element of COMPLEX holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX for r being Element of COMPLEX holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) let r be Element of COMPLEX ; ::_thesis: r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) A1: dom (r (#) (f1 - f2)) = dom (f1 - f2) by Th4 .= (dom f1) /\ (dom f2) by Th2 .= (dom f1) /\ (dom (r (#) f2)) by Th4 .= (dom (r (#) f1)) /\ (dom (r (#) f2)) by Th4 .= dom ((r (#) f1) - (r (#) f2)) by Th2 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(r_(#)_(f1_-_f2))_holds_ (r_(#)_(f1_-_f2))_/._c_=_((r_(#)_f1)_-_(r_(#)_f2))_/._c let c be Element of C; ::_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 Th4; A4: c in (dom (r (#) f1)) /\ (dom (r (#) f2)) by A1, A2, Th2; 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, Th4 .= r * ((f1 /. c) - (f2 /. c)) by A3, Th2 .= (r * (f1 /. c)) - (r * (f2 /. c)) .= ((r (#) f1) /. c) - (r * (f2 /. c)) by A5, Th4 .= ((r (#) f1) /. c) - ((r (#) f2) /. c) by A6, Th4 .= ((r (#) f1) - (r (#) f2)) /. c by A1, A2, Th2 ; ::_thesis: verum end; hence r (#) (f1 - f2) = (r (#) f1) - (r (#) f2) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: CFUNCT_1:24 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX holds f1 - f2 = (- 1r) (#) (f2 - f1) proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds f1 - f2 = (- 1r) (#) (f2 - f1) let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: f1 - f2 = (- 1r) (#) (f2 - f1) A1: dom (f1 - f2) = (dom f2) /\ (dom f1) by Th2 .= dom (f2 - f1) by Th2 .= dom ((- 1r) (#) (f2 - f1)) by Th4 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_f2)_holds_ (f1_-_f2)_/._c_=_((-_1r)_(#)_(f2_-_f1))_/._c A2: dom (f1 - f2) = (dom f2) /\ (dom f1) by Th2 .= dom (f2 - f1) by Th2 ; let c be Element of C; ::_thesis: ( c in dom (f1 - f2) implies (f1 - f2) /. c = ((- 1r) (#) (f2 - f1)) /. c ) assume A3: c in dom (f1 - f2) ; ::_thesis: (f1 - f2) /. c = ((- 1r) (#) (f2 - f1)) /. c thus (f1 - f2) /. c = (f1 /. c) - (f2 /. c) by A3, Th2 .= (- 1) * ((f2 /. c) - (f1 /. c)) .= (- 1r) * ((f2 - f1) /. c) by A3, A2, Th2, COMPLEX1:def_4 .= ((- 1r) (#) (f2 - f1)) /. c by A1, A3, Th4 ; ::_thesis: verum end; hence f1 - f2 = (- 1r) (#) (f2 - f1) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: CFUNCT_1:25 for C being non empty set for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 - (f2 + f3) = (f1 - f2) - f3 proof let C be non empty set ; ::_thesis: for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 - (f2 + f3) = (f1 - f2) - f3 let f1, f2, f3 be PartFunc of C,COMPLEX; ::_thesis: f1 - (f2 + f3) = (f1 - f2) - f3 A1: dom (f1 - (f2 + f3)) = (dom f1) /\ (dom (f2 + f3)) by Th2 .= (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 Th2 .= dom ((f1 - f2) - f3) by Th2 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_(f2_+_f3))_holds_ (f1_-_(f2_+_f3))_/._c_=_((f1_-_f2)_-_f3)_/._c let c be Element of C; ::_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 Th2; then A3: c in dom (f2 + f3) by XBOOLE_0:def_4; c in (dom (f1 - f2)) /\ (dom f3) by A1, A2, Th2; then A4: c in dom (f1 - f2) by XBOOLE_0:def_4; thus (f1 - (f2 + f3)) /. c = (f1 /. c) - ((f2 + f3) /. c) by A2, Th2 .= (f1 /. c) - ((f2 /. c) + (f3 /. c)) by A3, Th1 .= ((f1 /. c) - (f2 /. c)) - (f3 /. c) .= ((f1 - f2) /. c) - (f3 /. c) by A4, Th2 .= ((f1 - f2) - f3) /. c by A1, A2, Th2 ; ::_thesis: verum end; hence f1 - (f2 + f3) = (f1 - f2) - f3 by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: CFUNCT_1:26 for C being non empty set for f being PartFunc of C,COMPLEX holds 1r (#) f = f proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds 1r (#) f = f let f be PartFunc of C,COMPLEX; ::_thesis: 1r (#) f = f A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(1r_(#)_f)_holds_ (1r_(#)_f)_/._c_=_f_/._c let c be Element of C; ::_thesis: ( c in dom (1r (#) f) implies (1r (#) f) /. c = f /. c ) assume c in dom (1r (#) f) ; ::_thesis: (1r (#) f) /. c = f /. c hence (1r (#) f) /. c = 1r * (f /. c) by Th4 .= f /. c by COMPLEX1:def_4 ; ::_thesis: verum end; dom (1r (#) f) = dom f by Th4; hence 1r (#) f = f by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: CFUNCT_1:27 for C being non empty set for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 - (f2 - f3) = (f1 - f2) + f3 proof let C be non empty set ; ::_thesis: for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 - (f2 - f3) = (f1 - f2) + f3 let f1, f2, f3 be PartFunc of C,COMPLEX; ::_thesis: f1 - (f2 - f3) = (f1 - f2) + f3 A1: dom (f1 - (f2 - f3)) = (dom f1) /\ (dom (f2 - f3)) by Th2 .= (dom f1) /\ ((dom f2) /\ (dom f3)) by Th2 .= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16 .= (dom (f1 - f2)) /\ (dom f3) by Th2 .= dom ((f1 - f2) + f3) by VALUED_1:def_1 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_-_(f2_-_f3))_holds_ (f1_-_(f2_-_f3))_/._c_=_((f1_-_f2)_+_f3)_/._c let c be Element of C; ::_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 A1, VALUED_1:def_1; then A3: c in dom (f1 - f2) by XBOOLE_0:def_4; c in (dom f1) /\ (dom (f2 - f3)) by A2, Th2; then A4: c in dom (f2 - f3) by XBOOLE_0:def_4; thus (f1 - (f2 - f3)) /. c = (f1 /. c) - ((f2 - f3) /. c) by A2, Th2 .= (f1 /. c) - ((f2 /. c) - (f3 /. c)) by A4, Th2 .= ((f1 /. c) - (f2 /. c)) + (f3 /. c) .= ((f1 - f2) /. c) + (f3 /. c) by A3, Th2 .= ((f1 - f2) + f3) /. c by A1, A2, Th1 ; ::_thesis: verum end; hence f1 - (f2 - f3) = (f1 - f2) + f3 by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: CFUNCT_1:28 for C being non empty set for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 + (f2 - f3) = (f1 + f2) - f3 proof let C be non empty set ; ::_thesis: for f1, f2, f3 being PartFunc of C,COMPLEX holds f1 + (f2 - f3) = (f1 + f2) - f3 let f1, f2, f3 be PartFunc of C,COMPLEX; ::_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 Th2 .= ((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 Th2 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f1_+_(f2_-_f3))_holds_ (f1_+_(f2_-_f3))_/._c_=_((f1_+_f2)_-_f3)_/._c let c be Element of C; ::_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, Th2; then A4: c in dom (f1 + f2) by XBOOLE_0:def_4; thus (f1 + (f2 - f3)) /. c = (f1 /. c) + ((f2 - f3) /. c) by A2, Th1 .= (f1 /. c) + ((f2 /. c) - (f3 /. c)) by A3, Th2 .= ((f1 /. c) + (f2 /. c)) - (f3 /. c) .= ((f1 + f2) /. c) - (f3 /. c) by A4, Th1 .= ((f1 + f2) - f3) /. c by A1, A2, Th2 ; ::_thesis: verum end; hence f1 + (f2 - f3) = (f1 + f2) - f3 by A1, PARTFUN2:1; ::_thesis: verum end; theorem Th29: :: CFUNCT_1:29 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX holds |.(f1 (#) f2).| = |.f1.| (#) |.f2.| proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds |.(f1 (#) f2).| = |.f1.| (#) |.f2.| let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: |.(f1 (#) f2).| = |.f1.| (#) |.f2.| A1: dom |.(f1 (#) f2).| = dom (f1 (#) f2) by VALUED_1:def_11 .= (dom f1) /\ (dom f2) by Th3 .= (dom f1) /\ (dom |.f2.|) by VALUED_1:def_11 .= (dom |.f1.|) /\ (dom |.f2.|) by VALUED_1:def_11 .= dom (|.f1.| (#) |.f2.|) by VALUED_1:def_4 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_|.(f1_(#)_f2).|_holds_ |.(f1_(#)_f2).|_._c_=_(|.f1.|_(#)_|.f2.|)_._c A2: dom |.f2.| = dom f2 by VALUED_1:def_11; let c be Element of C; ::_thesis: ( c in dom |.(f1 (#) f2).| implies |.(f1 (#) f2).| . c = (|.f1.| (#) |.f2.|) . c ) A3: dom |.f1.| = dom f1 by VALUED_1:def_11; assume A4: c in dom |.(f1 (#) f2).| ; ::_thesis: |.(f1 (#) f2).| . c = (|.f1.| (#) |.f2.|) . c then A5: c in dom (f1 (#) f2) by VALUED_1:def_11; A6: c in (dom |.f1.|) /\ (dom |.f2.|) by A1, A4, VALUED_1:def_4; then c in dom |.f1.| by XBOOLE_0:def_4; then A7: f1 . c = f1 /. c by A3, PARTFUN1:def_6; c in dom |.f2.| by A6, XBOOLE_0:def_4; then A8: f2 /. c = f2 . c by A2, PARTFUN1:def_6; thus |.(f1 (#) f2).| . c = |.((f1 (#) f2) . c).| by VALUED_1:18 .= |.((f1 (#) f2) /. c).| by A5, PARTFUN1:def_6 .= |.((f1 /. c) * (f2 /. c)).| by A5, Th3 .= |.(f1 /. c).| * |.(f2 /. c).| by COMPLEX1:65 .= (|.f1.| . c) * |.(f2 /. c).| by A7, VALUED_1:18 .= (|.f1.| . c) * (|.f2.| . c) by A8, VALUED_1:18 .= (|.f1.| (#) |.f2.|) . c by VALUED_1:5 ; ::_thesis: verum end; hence |.(f1 (#) f2).| = |.f1.| (#) |.f2.| by A1, PARTFUN1:5; ::_thesis: verum end; theorem Th30: :: CFUNCT_1:30 for C being non empty set for f being PartFunc of C,COMPLEX for r being Element of COMPLEX holds |.(r (#) f).| = |.r.| (#) |.f.| proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX for r being Element of COMPLEX holds |.(r (#) f).| = |.r.| (#) |.f.| let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds |.(r (#) f).| = |.r.| (#) |.f.| let r be Element of COMPLEX ; ::_thesis: |.(r (#) f).| = |.r.| (#) |.f.| A1: dom f = dom |.f.| by VALUED_1:def_11; A2: dom |.(r (#) f).| = dom (r (#) f) by VALUED_1:def_11 .= dom f by Th4 .= dom (|.r.| (#) |.f.|) by A1, VALUED_1:def_5 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_|.(r_(#)_f).|_holds_ |.(r_(#)_f).|_._c_=_(|.r.|_(#)_|.f.|)_._c let c be Element of C; ::_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) by VALUED_1:def_11; A5: c in dom |.f.| by A2, A3, VALUED_1:def_5; thus |.(r (#) f).| . c = |.((r (#) f) . c).| by VALUED_1:18 .= |.((r (#) f) /. c).| by A4, PARTFUN1:def_6 .= |.(r * (f /. c)).| by A4, Th4 .= |.r.| * |.(f /. c).| by COMPLEX1:65 .= |.r.| * |.(f . c).| by A1, A5, PARTFUN1:def_6 .= |.r.| * (|.f.| . c) by VALUED_1:18 .= (|.r.| (#) |.f.|) . c by A2, A3, VALUED_1:def_5 ; ::_thesis: verum end; hence |.(r (#) f).| = |.r.| (#) |.f.| by A2, PARTFUN1:5; ::_thesis: verum end; theorem :: CFUNCT_1:31 for C being non empty set for f being PartFunc of C,COMPLEX holds - f = (- 1r) (#) f by COMPLEX1:def_4; theorem :: CFUNCT_1:32 canceled; theorem :: CFUNCT_1:33 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX holds f1 - (- f2) = f1 + f2 ; theorem Th34: :: CFUNCT_1:34 for C being non empty set for f being PartFunc of C,COMPLEX holds (f ^) ^ = f | (dom (f ^)) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds (f ^) ^ = f | (dom (f ^)) let f be PartFunc of C,COMPLEX; ::_thesis: (f ^) ^ = f | (dom (f ^)) A1: dom ((f ^) ^) = dom (f | (dom (f ^))) by Th11; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f_^)_^)_holds_ ((f_^)_^)_/._c_=_(f_|_(dom_(f_^)))_/._c let c be Element of C; ::_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, PARTFUN2:15 ; ::_thesis: verum end; hence (f ^) ^ = f | (dom (f ^)) by A1, PARTFUN2:1; ::_thesis: verum end; theorem Th35: :: CFUNCT_1:35 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX holds (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^) proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^) let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^) A1: dom ((f1 (#) f2) ^) = (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0c}) by Def2 .= ((dom f1) \ (f1 " {0c})) /\ ((dom f2) \ (f2 " {0c})) by Th7 .= (dom (f1 ^)) /\ ((dom f2) \ (f2 " {0c})) by Def2 .= (dom (f1 ^)) /\ (dom (f2 ^)) by Def2 .= dom ((f1 ^) (#) (f2 ^)) by Th3 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_^)_holds_ ((f1_(#)_f2)_^)_/._c_=_((f1_^)_(#)_(f2_^))_/._c let c be Element of C; ::_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 c in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0c}) by Def2; then A3: c in dom (f1 (#) f2) by XBOOLE_0:def_5; A4: c in (dom (f1 ^)) /\ (dom (f2 ^)) by A1, A2, Th3; 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 (#) f2) /. c) " by A2, Def2 .= ((f1 /. c) * (f2 /. c)) " by A3, Th3 .= ((f1 /. c) ") * ((f2 /. c) ") by XCMPLX_1:204 .= ((f1 ^) /. c) * ((f2 /. c) ") by A5, Def2 .= ((f1 ^) /. c) * ((f2 ^) /. c) by A6, Def2 .= ((f1 ^) (#) (f2 ^)) /. c by A1, A2, Th3 ; ::_thesis: verum end; hence (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^) by A1, PARTFUN2:1; ::_thesis: verum end; theorem Th36: :: CFUNCT_1:36 for C being non empty set for f being PartFunc of C,COMPLEX for r being Element of COMPLEX st r <> 0 holds (r (#) f) ^ = (r ") (#) (f ^) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX for r being Element of COMPLEX st r <> 0 holds (r (#) f) ^ = (r ") (#) (f ^) let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX st r <> 0 holds (r (#) f) ^ = (r ") (#) (f ^) let r be Element of COMPLEX ; ::_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) " {0c}) by Def2 .= (dom (r (#) f)) \ (f " {0c}) by A1, Th12 .= (dom f) \ (f " {0c}) by Th4 .= dom (f ^) by Def2 .= dom ((r ") (#) (f ^)) by Th4 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((r_(#)_f)_^)_holds_ ((r_(#)_f)_^)_/._c_=_((r_")_(#)_(f_^))_/._c let c be Element of C; ::_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 (f ^) by A2, Th4; c in (dom (r (#) f)) \ ((r (#) f) " {0c}) by A3, Def2; then A5: c in dom (r (#) f) by XBOOLE_0:def_5; thus ((r (#) f) ^) /. c = ((r (#) f) /. c) " by A3, Def2 .= (r * (f /. c)) " by A5, Th4 .= (r ") * ((f /. c) ") by XCMPLX_1:204 .= (r ") * ((f ^) /. c) by A4, Def2 .= ((r ") (#) (f ^)) /. c by A2, A3, Th4 ; ::_thesis: verum end; hence (r (#) f) ^ = (r ") (#) (f ^) by A2, PARTFUN2:1; ::_thesis: verum end; Lm2: (- 1r) " = - 1r by COMPLEX1:def_4; theorem :: CFUNCT_1:37 for C being non empty set for f being PartFunc of C,COMPLEX holds (- f) ^ = (- 1r) (#) (f ^) by Lm2, Th36, COMPLEX1:def_4; theorem Th38: :: CFUNCT_1:38 for C being non empty set for f being PartFunc of C,COMPLEX holds |.f.| ^ = |.(f ^).| proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds |.f.| ^ = |.(f ^).| let f be PartFunc of C,COMPLEX; ::_thesis: |.f.| ^ = |.(f ^).| A1: dom (|.f.| ^) = (dom |.f.|) \ (|.f.| " {0}) by RFUNCT_1:def_2 .= (dom f) \ (|.f.| " {0}) by VALUED_1:def_11 .= (dom f) \ (f " {0c}) by Th10 .= dom (f ^) by Def2 .= dom |.(f ^).| by VALUED_1:def_11 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(|.f.|_^)_holds_ (|.f.|_^)_._c_=_|.(f_^).|_._c let c be Element of C; ::_thesis: ( c in dom (|.f.| ^) implies (|.f.| ^) . c = |.(f ^).| . c ) A2: dom f = dom |.f.| by VALUED_1:def_11; assume A3: c in dom (|.f.| ^) ; ::_thesis: (|.f.| ^) . c = |.(f ^).| . c then A4: c in dom (f ^) by A1, VALUED_1:def_11; c in (dom |.f.|) \ (|.f.| " {0}) by A3, RFUNCT_1:def_2; then A5: c in dom |.f.| by XBOOLE_0:def_5; thus (|.f.| ^) . c = (|.f.| . c) " by A3, RFUNCT_1:def_2 .= |.(f . c).| " by VALUED_1:18 .= |.(f /. c).| " by A5, A2, PARTFUN1:def_6 .= |.1r.| / |.(f /. c).| by COMPLEX1:48, XCMPLX_1:215 .= |.(1r / (f /. c)).| by COMPLEX1:67 .= |.((f /. c) ").| by COMPLEX1:def_4, XCMPLX_1:215 .= |.((f ^) /. c).| by A4, Def2 .= |.((f ^) . c).| by A4, PARTFUN1:def_6 .= |.(f ^).| . c by VALUED_1:18 ; ::_thesis: verum end; hence |.f.| ^ = |.(f ^).| by A1, PARTFUN1:5; ::_thesis: verum end; theorem Th39: :: CFUNCT_1:39 for C being non empty set for f, g being PartFunc of C,COMPLEX holds f / g = f (#) (g ^) proof let C be non empty set ; ::_thesis: for f, g being PartFunc of C,COMPLEX holds f / g = f (#) (g ^) let f, g be PartFunc of C,COMPLEX; ::_thesis: f / g = f (#) (g ^) A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(f_/_g)_holds_ (f_/_g)_/._c_=_(f_(#)_(g_^))_/._c let c be Element of C; ::_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 " {0c})) by Def1; then A3: c in (dom f) /\ (dom (g ^)) by Def2; then A4: c in dom (g ^) by XBOOLE_0:def_4; A5: c in dom (f (#) (g ^)) by A3, Th3; thus (f / g) /. c = (f /. c) * ((g /. c) ") by A2, Def1 .= (f /. c) * ((g ^) /. c) by A4, Def2 .= (f (#) (g ^)) /. c by A5, Th3 ; ::_thesis: verum end; dom (f / g) = (dom f) /\ ((dom g) \ (g " {0c})) by Def1 .= (dom f) /\ (dom (g ^)) by Def2 .= dom (f (#) (g ^)) by Th3 ; hence f / g = f (#) (g ^) by A1, PARTFUN2:1; ::_thesis: verum end; theorem Th40: :: CFUNCT_1:40 for C being non empty set for g, f being PartFunc of C,COMPLEX for r being Element of COMPLEX holds r (#) (g / f) = (r (#) g) / f proof let C be non empty set ; ::_thesis: for g, f being PartFunc of C,COMPLEX for r being Element of COMPLEX holds r (#) (g / f) = (r (#) g) / f let g, f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds r (#) (g / f) = (r (#) g) / f let r be Element of COMPLEX ; ::_thesis: r (#) (g / f) = (r (#) g) / f thus r (#) (g / f) = r (#) (g (#) (f ^)) by Th39 .= (r (#) g) (#) (f ^) by Th17 .= (r (#) g) / f by Th39 ; ::_thesis: verum end; theorem :: CFUNCT_1:41 for C being non empty set for f, g being PartFunc of C,COMPLEX holds (f / g) (#) g = f | (dom (g ^)) proof let C be non empty set ; ::_thesis: for f, g being PartFunc of C,COMPLEX holds (f / g) (#) g = f | (dom (g ^)) let f, g be PartFunc of C,COMPLEX; ::_thesis: (f / g) (#) g = f | (dom (g ^)) A1: dom ((f / g) (#) g) = (dom (f / g)) /\ (dom g) by Th3 .= ((dom f) /\ ((dom g) \ (g " {0c}))) /\ (dom g) by Def1 .= (dom f) /\ (((dom g) \ (g " {0c})) /\ (dom g)) by XBOOLE_1:16 .= (dom f) /\ ((dom (g ^)) /\ (dom g)) by Def2 .= (dom f) /\ (dom (g ^)) by Th6, XBOOLE_1:28 .= dom (f | (dom (g ^))) by RELAT_1:61 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f_/_g)_(#)_g)_holds_ ((f_/_g)_(#)_g)_/._c_=_(f_|_(dom_(g_^)))_/._c let c be Element of C; ::_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 A3: c in (dom f) /\ (dom (g ^)) by A1, RELAT_1:61; then A4: c in dom (f (#) (g ^)) by Th3; A5: c in dom (g ^) by A3, XBOOLE_0:def_4; then A6: g /. c <> 0c by Th8; thus ((f / g) (#) g) /. c = ((f / g) /. c) * (g /. c) by A2, Th3 .= ((f (#) (g ^)) /. c) * (g /. c) by Th39 .= ((f /. c) * ((g ^) /. c)) * (g /. c) by A4, Th3 .= ((f /. c) * ((g /. c) ")) * (g /. c) by A5, Def2 .= (f /. c) * (((g /. c) ") * (g /. c)) .= (f /. c) * 1r by A6, COMPLEX1:def_4, XCMPLX_0:def_7 .= (f | (dom (g ^))) /. c by A1, A2, COMPLEX1:def_4, PARTFUN2:15 ; ::_thesis: verum end; hence (f / g) (#) g = f | (dom (g ^)) by A1, PARTFUN2:1; ::_thesis: verum end; theorem Th42: :: CFUNCT_1:42 for C being non empty set for f, g, f1, g1 being PartFunc of C,COMPLEX holds (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1) proof let C be non empty set ; ::_thesis: for f, g, f1, g1 being PartFunc of C,COMPLEX holds (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1) let f, g, f1, g1 be PartFunc of C,COMPLEX; ::_thesis: (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1) A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f_/_g)_(#)_(f1_/_g1))_holds_ ((f_/_g)_(#)_(f1_/_g1))_/._c_=_((f_(#)_f1)_/_(g_(#)_g1))_/._c let c be Element of C; ::_thesis: ( c in dom ((f / g) (#) (f1 / g1)) implies ((f / g) (#) (f1 / g1)) /. c = ((f (#) f1) / (g (#) g1)) /. c ) assume A2: c in dom ((f / g) (#) (f1 / g1)) ; ::_thesis: ((f / g) (#) (f1 / g1)) /. c = ((f (#) f1) / (g (#) g1)) /. c then c in (dom (f / g)) /\ (dom (f1 / g1)) by Th3; then A3: c in (dom (f (#) (g ^))) /\ (dom (f1 / g1)) by Th39; then A4: c in dom (f (#) (g ^)) by XBOOLE_0:def_4; then A5: c in (dom f) /\ (dom (g ^)) by Th3; c in (dom (f (#) (g ^))) /\ (dom (f1 (#) (g1 ^))) by A3, Th39; then A6: c in dom (f1 (#) (g1 ^)) by XBOOLE_0:def_4; then A7: c in (dom f1) /\ (dom (g1 ^)) by Th3; then A8: c in dom f1 by XBOOLE_0:def_4; c in dom f by A5, XBOOLE_0:def_4; then c in (dom f) /\ (dom f1) by A8, XBOOLE_0:def_4; then A9: c in dom (f (#) f1) by Th3; A10: c in dom (g1 ^) by A7, XBOOLE_0:def_4; c in dom (g ^) by A5, XBOOLE_0:def_4; then c in (dom (g ^)) /\ (dom (g1 ^)) by A10, XBOOLE_0:def_4; then A11: c in dom ((g ^) (#) (g1 ^)) by Th3; then c in dom ((g (#) g1) ^) by Th35; then c in (dom (f (#) f1)) /\ (dom ((g (#) g1) ^)) by A9, XBOOLE_0:def_4; then A12: c in dom ((f (#) f1) (#) ((g (#) g1) ^)) by Th3; thus ((f / g) (#) (f1 / g1)) /. c = ((f / g) /. c) * ((f1 / g1) /. c) by A2, Th3 .= ((f (#) (g ^)) /. c) * ((f1 / g1) /. c) by Th39 .= ((f (#) (g ^)) /. c) * ((f1 (#) (g1 ^)) /. c) by Th39 .= ((f /. c) * ((g ^) /. c)) * ((f1 (#) (g1 ^)) /. c) by A4, Th3 .= ((f /. c) * ((g ^) /. c)) * ((f1 /. c) * ((g1 ^) /. c)) by A6, Th3 .= (f /. c) * ((f1 /. c) * (((g ^) /. c) * ((g1 ^) /. c))) .= (f /. c) * ((f1 /. c) * (((g ^) (#) (g1 ^)) /. c)) by A11, Th3 .= ((f /. c) * (f1 /. c)) * (((g ^) (#) (g1 ^)) /. c) .= ((f /. c) * (f1 /. c)) * (((g (#) g1) ^) /. c) by Th35 .= ((f (#) f1) /. c) * (((g (#) g1) ^) /. c) by A9, Th3 .= ((f (#) f1) (#) ((g (#) g1) ^)) /. c by A12, Th3 .= ((f (#) f1) / (g (#) g1)) /. c by Th39 ; ::_thesis: verum end; dom ((f / g) (#) (f1 / g1)) = (dom (f / g)) /\ (dom (f1 / g1)) by Th3 .= ((dom f) /\ ((dom g) \ (g " {0c}))) /\ (dom (f1 / g1)) by Def1 .= ((dom f) /\ ((dom g) \ (g " {0c}))) /\ ((dom f1) /\ ((dom g1) \ (g1 " {0c}))) by Def1 .= (dom f) /\ (((dom g) \ (g " {0c})) /\ ((dom f1) /\ ((dom g1) \ (g1 " {0c})))) by XBOOLE_1:16 .= (dom f) /\ ((dom f1) /\ (((dom g) \ (g " {0c})) /\ ((dom g1) \ (g1 " {0c})))) by XBOOLE_1:16 .= ((dom f) /\ (dom f1)) /\ (((dom g) \ (g " {0c})) /\ ((dom g1) \ (g1 " {0c}))) by XBOOLE_1:16 .= (dom (f (#) f1)) /\ (((dom g) \ (g " {0c})) /\ ((dom g1) \ (g1 " {0c}))) by Th3 .= (dom (f (#) f1)) /\ ((dom (g (#) g1)) \ ((g (#) g1) " {0c})) by Th7 .= dom ((f (#) f1) / (g (#) g1)) by Def1 ; hence (f / g) (#) (f1 / g1) = (f (#) f1) / (g (#) g1) by A1, PARTFUN2:1; ::_thesis: verum end; theorem Th43: :: CFUNCT_1:43 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX holds (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1 proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1 let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: (f1 / f2) ^ = (f2 | (dom (f2 ^))) / f1 thus (f1 / f2) ^ = (f1 (#) (f2 ^)) ^ by Th39 .= (f1 ^) (#) ((f2 ^) ^) by Th35 .= (f2 | (dom (f2 ^))) (#) (f1 ^) by Th34 .= (f2 | (dom (f2 ^))) / f1 by Th39 ; ::_thesis: verum end; theorem Th44: :: CFUNCT_1:44 for C being non empty set for g, f1, f2 being PartFunc of C,COMPLEX holds g (#) (f1 / f2) = (g (#) f1) / f2 proof let C be non empty set ; ::_thesis: for g, f1, f2 being PartFunc of C,COMPLEX holds g (#) (f1 / f2) = (g (#) f1) / f2 let g, f1, f2 be PartFunc of C,COMPLEX; ::_thesis: g (#) (f1 / f2) = (g (#) f1) / f2 thus g (#) (f1 / f2) = g (#) (f1 (#) (f2 ^)) by Th39 .= (g (#) f1) (#) (f2 ^) by Th14 .= (g (#) f1) / f2 by Th39 ; ::_thesis: verum end; theorem :: CFUNCT_1:45 for C being non empty set for g, f1, f2 being PartFunc of C,COMPLEX holds g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1 proof let C be non empty set ; ::_thesis: for g, f1, f2 being PartFunc of C,COMPLEX holds g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1 let g, f1, f2 be PartFunc of C,COMPLEX; ::_thesis: g / (f1 / f2) = (g (#) (f2 | (dom (f2 ^)))) / f1 thus g / (f1 / f2) = g (#) ((f1 / f2) ^) by Th39 .= g (#) ((f2 | (dom (f2 ^))) / f1) by Th43 .= (g (#) (f2 | (dom (f2 ^)))) / f1 by Th44 ; ::_thesis: verum end; theorem :: CFUNCT_1:46 for C being non empty set for f, g being PartFunc of C,COMPLEX holds ( - (f / g) = (- f) / g & f / (- g) = - (f / g) ) proof let C be non empty set ; ::_thesis: for f, g being PartFunc of C,COMPLEX holds ( - (f / g) = (- f) / g & f / (- g) = - (f / g) ) let f, g be PartFunc of C,COMPLEX; ::_thesis: ( - (f / g) = (- f) / g & f / (- g) = - (f / g) ) thus - (f / g) = (- 1r) (#) (f / g) by COMPLEX1:def_4 .= (- f) / g by Th40, COMPLEX1:def_4 ; ::_thesis: f / (- g) = - (f / g) thus f / (- g) = f (#) ((- g) ^) by Th39 .= f (#) ((- 1r) (#) (g ^)) by Lm2, Th36, COMPLEX1:def_4 .= - (f (#) (g ^)) by Th18, COMPLEX1:def_4 .= - (f / g) by Th39 ; ::_thesis: verum end; theorem :: CFUNCT_1:47 for C being non empty set for f1, f, f2 being PartFunc of C,COMPLEX holds ( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f ) proof let C be non empty set ; ::_thesis: for f1, f, f2 being PartFunc of C,COMPLEX holds ( (f1 / f) + (f2 / f) = (f1 + f2) / f & (f1 / f) - (f2 / f) = (f1 - f2) / f ) let f1, f, f2 be PartFunc of C,COMPLEX; ::_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 Th39 .= (f1 (#) (f ^)) + (f2 (#) (f ^)) by Th39 .= (f1 + f2) (#) (f ^) by Th15 .= (f1 + f2) / f by Th39 ; ::_thesis: (f1 / f) - (f2 / f) = (f1 - f2) / f thus (f1 / f) - (f2 / f) = (f1 (#) (f ^)) - (f2 / f) by Th39 .= (f1 (#) (f ^)) - (f2 (#) (f ^)) by Th39 .= (f1 - f2) (#) (f ^) by Th19 .= (f1 - f2) / f by Th39 ; ::_thesis: verum end; theorem Th48: :: CFUNCT_1:48 for C being non empty set for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g) proof let C be non empty set ; ::_thesis: for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g) let f1, f, g1, g be PartFunc of C,COMPLEX; ::_thesis: (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g) A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_/_f)_+_(g1_/_g))_holds_ ((f1_/_f)_+_(g1_/_g))_/._c_=_(((f1_(#)_g)_+_(g1_(#)_f))_/_(f_(#)_g))_/._c let c be Element of C; ::_thesis: ( c in dom ((f1 / f) + (g1 / g)) implies ((f1 / f) + (g1 / g)) /. c = (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) /. c ) A2: dom (f ^) c= dom f by Th6; 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: c in (dom (f1 (#) (f ^))) /\ (dom (g1 / g)) by A4, Th39; then c in dom (f1 (#) (f ^)) by XBOOLE_0:def_4; then A8: c in (dom f1) /\ (dom (f ^)) by Th3; then A9: c in dom (f ^) by XBOOLE_0:def_4; then A10: f /. c <> 0c by Th8; c in (dom (f1 (#) (f ^))) /\ (dom (g1 (#) (g ^))) by A7, Th39; then c in dom (g1 (#) (g ^)) by XBOOLE_0:def_4; then A11: c in (dom g1) /\ (dom (g ^)) by Th3; then A12: c in dom (g ^) by XBOOLE_0:def_4; then A13: g /. c <> 0c by Th8; c in dom g1 by A11, XBOOLE_0:def_4; then c in (dom g1) /\ (dom f) by A9, A2, XBOOLE_0:def_4; then A14: c in dom (g1 (#) f) by Th3; A15: dom (g ^) c= dom g by Th6; then c in (dom f) /\ (dom g) by A9, A12, A2, XBOOLE_0:def_4; then A16: c in dom (f (#) g) by Th3; c in dom f1 by A8, XBOOLE_0:def_4; then c in (dom f1) /\ (dom g) by A12, A15, XBOOLE_0:def_4; then A17: c in dom (f1 (#) g) by Th3; then c in (dom (f1 (#) g)) /\ (dom (g1 (#) f)) by A14, XBOOLE_0:def_4; then A18: c in dom ((f1 (#) g) + (g1 (#) f)) by VALUED_1:def_1; c in (dom (f ^)) /\ (dom (g ^)) by A9, A12, XBOOLE_0:def_4; then c in dom ((f ^) (#) (g ^)) by Th3; then c in dom ((f (#) g) ^) by Th35; then c in (dom ((f1 (#) g) + (g1 (#) f))) /\ (dom ((f (#) g) ^)) by A18, XBOOLE_0:def_4; then c in dom (((f1 (#) g) + (g1 (#) f)) (#) ((f (#) g) ^)) by Th3; then A19: c in dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) by Th39; thus ((f1 / f) + (g1 / g)) /. c = ((f1 / f) /. c) + ((g1 / g) /. c) by A3, Th1 .= ((f1 /. c) * ((f /. c) ")) + ((g1 / g) /. c) by A5, Def1 .= ((f1 /. c) * (1r * ((f /. c) "))) + (((g1 /. c) * 1r) * ((g /. c) ")) by A6, Def1, COMPLEX1:def_4 .= ((f1 /. c) * (((g /. c) * ((g /. c) ")) * ((f /. c) "))) + ((g1 /. c) * (1r * ((g /. c) "))) by A13, COMPLEX1:def_4, XCMPLX_0:def_7 .= ((f1 /. c) * ((g /. c) * (((g /. c) ") * ((f /. c) ")))) + ((g1 /. c) * (((f /. c) * ((f /. c) ")) * ((g /. c) "))) by A10, COMPLEX1:def_4, 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 A16, Th3 .= (((f1 /. c) * (g /. c)) * (((f (#) g) /. c) ")) + ((g1 /. c) * ((f /. c) * (((f (#) g) /. c) "))) by A16, Th3 .= (((f1 (#) g) /. c) * (((f (#) g) /. c) ")) + (((g1 /. c) * (f /. c)) * (((f (#) g) /. c) ")) by A17, Th3 .= (((f1 (#) g) /. c) * (((f (#) g) /. c) ")) + (((g1 (#) f) /. c) * (((f (#) g) /. c) ")) by A14, Th3 .= (((f1 (#) g) /. c) + ((g1 (#) f) /. c)) * (((f (#) g) /. c) ") .= (((f1 (#) g) + (g1 (#) f)) /. c) * (((f (#) g) /. c) ") by A18, Th1 .= (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) /. c by A19, 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 " {0c}))) /\ (dom (g1 / g)) by Def1 .= ((dom f1) /\ ((dom f) \ (f " {0c}))) /\ ((dom g1) /\ ((dom g) \ (g " {0c}))) by Def1 .= ((dom f1) /\ ((dom f) /\ ((dom f) \ (f " {0c})))) /\ ((dom g1) /\ ((dom g) \ (g " {0c}))) by Th6 .= (((dom f) /\ ((dom f) \ (f " {0c}))) /\ (dom f1)) /\ (((dom g) /\ ((dom g) \ (g " {0c}))) /\ (dom g1)) by Th6 .= ((dom f) /\ ((dom f) \ (f " {0c}))) /\ ((dom f1) /\ (((dom g) /\ ((dom g) \ (g " {0c}))) /\ (dom g1))) by XBOOLE_1:16 .= ((dom f) /\ ((dom f) \ (f " {0c}))) /\ (((dom f1) /\ ((dom g) /\ ((dom g) \ (g " {0c})))) /\ (dom g1)) by XBOOLE_1:16 .= ((dom f) /\ ((dom f) \ (f " {0c}))) /\ ((((dom f1) /\ (dom g)) /\ ((dom g) \ (g " {0c}))) /\ (dom g1)) by XBOOLE_1:16 .= ((dom f) /\ ((dom f) \ (f " {0c}))) /\ (((dom (f1 (#) g)) /\ ((dom g) \ (g " {0c}))) /\ (dom g1)) by Th3 .= ((dom f) /\ ((dom f) \ (f " {0c}))) /\ ((dom (f1 (#) g)) /\ ((dom g1) /\ ((dom g) \ (g " {0c})))) by XBOOLE_1:16 .= (dom (f1 (#) g)) /\ ((((dom f) \ (f " {0c})) /\ (dom f)) /\ ((dom g1) /\ ((dom g) \ (g " {0c})))) by XBOOLE_1:16 .= (dom (f1 (#) g)) /\ (((dom f) \ (f " {0c})) /\ ((dom f) /\ ((dom g1) /\ ((dom g) \ (g " {0c}))))) by XBOOLE_1:16 .= (dom (f1 (#) g)) /\ (((dom f) \ (f " {0c})) /\ (((dom g1) /\ (dom f)) /\ ((dom g) \ (g " {0c})))) by XBOOLE_1:16 .= (dom (f1 (#) g)) /\ (((dom f) \ (f " {0c})) /\ ((dom (g1 (#) f)) /\ ((dom g) \ (g " {0c})))) by Th3 .= (dom (f1 (#) g)) /\ ((dom (g1 (#) f)) /\ (((dom f) \ (f " {0c})) /\ ((dom g) \ (g " {0c})))) by XBOOLE_1:16 .= ((dom (f1 (#) g)) /\ (dom (g1 (#) f))) /\ (((dom f) \ (f " {0c})) /\ ((dom g) \ (g " {0c}))) by XBOOLE_1:16 .= (dom ((f1 (#) g) + (g1 (#) f))) /\ (((dom f) \ (f " {0c})) /\ ((dom g) \ (g " {0c}))) by VALUED_1:def_1 .= (dom ((f1 (#) g) + (g1 (#) f))) /\ ((dom (f (#) g)) \ ((f (#) g) " {0c})) by Th7 .= dom (((f1 (#) g) + (g1 (#) f)) / (f (#) g)) by Def1 ; hence (f1 / f) + (g1 / g) = ((f1 (#) g) + (g1 (#) f)) / (f (#) g) by A1, PARTFUN2:1; ::_thesis: verum end; theorem :: CFUNCT_1:49 for C being non empty set for f, g, f1, g1 being PartFunc of C,COMPLEX holds (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1) proof let C be non empty set ; ::_thesis: for f, g, f1, g1 being PartFunc of C,COMPLEX holds (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1) let f, g, f1, g1 be PartFunc of C,COMPLEX; ::_thesis: (f / g) / (f1 / g1) = (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1) thus (f / g) / (f1 / g1) = (f / g) (#) ((f1 / g1) ^) by Th39 .= (f / g) (#) ((g1 | (dom (g1 ^))) / f1) by Th43 .= (f (#) (g1 | (dom (g1 ^)))) / (g (#) f1) by Th42 ; ::_thesis: verum end; theorem :: CFUNCT_1:50 for C being non empty set for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g) proof let C be non empty set ; ::_thesis: for f1, f, g1, g being PartFunc of C,COMPLEX holds (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g) let f1, f, g1, g be PartFunc of C,COMPLEX; ::_thesis: (f1 / f) - (g1 / g) = ((f1 (#) g) - (g1 (#) f)) / (f (#) g) thus (f1 / f) - (g1 / g) = (f1 / f) + (((- 1r) (#) g1) / g) by Th40, COMPLEX1:def_4 .= ((f1 (#) g) + (((- 1r) (#) g1) (#) f)) / (f (#) g) by Th48 .= ((f1 (#) g) - (g1 (#) f)) / (f (#) g) by Th17, COMPLEX1:def_4 ; ::_thesis: verum end; theorem :: CFUNCT_1:51 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX holds |.(f1 / f2).| = |.f1.| / |.f2.| proof let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds |.(f1 / f2).| = |.f1.| / |.f2.| let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: |.(f1 / f2).| = |.f1.| / |.f2.| thus |.(f1 / f2).| = |.(f1 (#) (f2 ^)).| by Th39 .= |.f1.| (#) |.(f2 ^).| by Th29 .= |.f1.| (#) (|.f2.| ^) by Th38 .= |.f1.| / |.f2.| by RFUNCT_1:31 ; ::_thesis: verum end; theorem Th52: :: CFUNCT_1:52 for X being set for C being non empty set for f1, f2 being PartFunc of C,COMPLEX 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 C being non empty set for f1, f2 being PartFunc of C,COMPLEX holds ( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) ) let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds ( (f1 + f2) | X = (f1 | X) + (f2 | X) & (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) ) let f1, f2 be PartFunc of C,COMPLEX; ::_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_Element_of_C_st_c_in_dom_((f1_+_f2)_|_X)_holds_ ((f1_+_f2)_|_X)_/._c_=_((f1_|_X)_+_(f2_|_X))_/._c let c be Element of C; ::_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, PARTFUN2:15 .= (f1 /. c) + (f2 /. c) by A5, Th1 .= ((f1 | X) /. c) + (f2 /. c) by A8, PARTFUN2:15 .= ((f1 | X) /. c) + ((f2 | X) /. c) by A7, PARTFUN2:15 .= ((f1 | X) + (f2 | X)) /. c by A9, Th1 ; ::_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, PARTFUN2:1; ::_thesis: ( (f1 + f2) | X = (f1 | X) + f2 & (f1 + f2) | X = f1 + (f2 | X) ) A10: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_|_X)_holds_ ((f1_+_f2)_|_X)_/._c_=_((f1_|_X)_+_f2)_/._c let c be Element of C; ::_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, PARTFUN2:15 .= (f1 /. c) + (f2 /. c) by A14, Th1 .= ((f1 | X) /. c) + (f2 /. c) by A16, PARTFUN2:15 .= ((f1 | X) + f2) /. c by A17, Th1 ; ::_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, PARTFUN2:1; ::_thesis: (f1 + f2) | X = f1 + (f2 | X) A18: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_+_f2)_|_X)_holds_ ((f1_+_f2)_|_X)_/._c_=_(f1_+_(f2_|_X))_/._c let c be Element of C; ::_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, PARTFUN2:15 .= (f1 /. c) + (f2 /. c) by A22, Th1 .= (f1 /. c) + ((f2 | X) /. c) by A24, PARTFUN2:15 .= (f1 + (f2 | X)) /. c by A25, Th1 ; ::_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, PARTFUN2:1; ::_thesis: verum end; theorem Th53: :: CFUNCT_1:53 for X being set for C being non empty set for f1, f2 being PartFunc of C,COMPLEX 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 C being non empty set for f1, f2 being PartFunc of C,COMPLEX holds ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) ) let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds ( (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) & (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) ) let f1, f2 be PartFunc of C,COMPLEX; ::_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_Element_of_C_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_ ((f1_(#)_f2)_|_X)_/._c_=_((f1_|_X)_(#)_(f2_|_X))_/._c let c be Element of C; ::_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 Th3; 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 Th3; thus ((f1 (#) f2) | X) /. c = (f1 (#) f2) /. c by A2, PARTFUN2:15 .= (f1 /. c) * (f2 /. c) by A5, Th3 .= ((f1 | X) /. c) * (f2 /. c) by A8, PARTFUN2:15 .= ((f1 | X) /. c) * ((f2 | X) /. c) by A7, PARTFUN2:15 .= ((f1 | X) (#) (f2 | X)) /. c by A9, Th3 ; ::_thesis: verum end; dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ (X /\ X) by Th3 .= (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 Th3 ; hence (f1 (#) f2) | X = (f1 | X) (#) (f2 | X) by A1, PARTFUN2:1; ::_thesis: ( (f1 (#) f2) | X = (f1 | X) (#) f2 & (f1 (#) f2) | X = f1 (#) (f2 | X) ) A10: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_ ((f1_(#)_f2)_|_X)_/._c_=_((f1_|_X)_(#)_f2)_/._c let c be Element of C; ::_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 Th3; 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 Th3; thus ((f1 (#) f2) | X) /. c = (f1 (#) f2) /. c by A11, PARTFUN2:15 .= (f1 /. c) * (f2 /. c) by A14, Th3 .= ((f1 | X) /. c) * (f2 /. c) by A16, PARTFUN2:15 .= ((f1 | X) (#) f2) /. c by A17, Th3 ; ::_thesis: verum end; dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ X by Th3 .= ((dom f1) /\ X) /\ (dom f2) by XBOOLE_1:16 .= (dom (f1 | X)) /\ (dom f2) by RELAT_1:61 .= dom ((f1 | X) (#) f2) by Th3 ; hence (f1 (#) f2) | X = (f1 | X) (#) f2 by A10, PARTFUN2:1; ::_thesis: (f1 (#) f2) | X = f1 (#) (f2 | X) A18: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f1_(#)_f2)_|_X)_holds_ ((f1_(#)_f2)_|_X)_/._c_=_(f1_(#)_(f2_|_X))_/._c let c be Element of C; ::_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 Th3; 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 Th3; thus ((f1 (#) f2) | X) /. c = (f1 (#) f2) /. c by A19, PARTFUN2:15 .= (f1 /. c) * (f2 /. c) by A22, Th3 .= (f1 /. c) * ((f2 | X) /. c) by A24, PARTFUN2:15 .= (f1 (#) (f2 | X)) /. c by A25, Th3 ; ::_thesis: verum end; dom ((f1 (#) f2) | X) = (dom (f1 (#) f2)) /\ X by RELAT_1:61 .= ((dom f1) /\ (dom f2)) /\ X by Th3 .= (dom f1) /\ ((dom f2) /\ X) by XBOOLE_1:16 .= (dom f1) /\ (dom (f2 | X)) by RELAT_1:61 .= dom (f1 (#) (f2 | X)) by Th3 ; hence (f1 (#) f2) | X = f1 (#) (f2 | X) by A18, PARTFUN2:1; ::_thesis: verum end; theorem Th54: :: CFUNCT_1:54 for X being set for C being non empty set for f being PartFunc of C,COMPLEX holds ( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & |.f.| | X = |.(f | X).| ) proof let X be set ; ::_thesis: for C being non empty set for f being PartFunc of C,COMPLEX holds ( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & |.f.| | X = |.(f | X).| ) let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds ( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & |.f.| | X = |.(f | X).| ) let f be PartFunc of C,COMPLEX; ::_thesis: ( (- f) | X = - (f | X) & (f ^) | X = (f | X) ^ & |.f.| | X = |.(f | X).| ) A1: dom ((f ^) | X) = (dom (f ^)) /\ X by RELAT_1:61 .= ((dom f) \ (f " {0c})) /\ X by Def2 .= ((dom f) /\ X) \ ((f " {0c}) /\ X) by XBOOLE_1:50 .= (dom (f | X)) \ (X /\ (f " {0c})) by RELAT_1:61 .= (dom (f | X)) \ ((f | X) " {0c}) by FUNCT_1:70 .= dom ((f | X) ^) by Def2 ; A2: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((-_f)_|_X)_holds_ ((-_f)_|_X)_/._c_=_(-_(f_|_X))_/._c let c be Element of C; ::_thesis: ( c in dom ((- f) | X) implies ((- f) | X) /. c = (- (f | X)) /. c ) assume A3: c in dom ((- f) | X) ; ::_thesis: ((- f) | X) /. c = (- (f | X)) /. c then A4: c in (dom (- f)) /\ X by RELAT_1:61; then A5: c in X by XBOOLE_0:def_4; A6: c in dom (- f) by A4, XBOOLE_0:def_4; then c in dom f by Th5; then c in (dom f) /\ X by A5, XBOOLE_0:def_4; then A7: c in dom (f | X) by RELAT_1:61; then A8: c in dom (- (f | X)) by Th5; thus ((- f) | X) /. c = (- f) /. c by A3, PARTFUN2:15 .= - (f /. c) by A6, Th5 .= - ((f | X) /. c) by A7, PARTFUN2:15 .= (- (f | X)) /. c by A8, Th5 ; ::_thesis: verum end; dom ((- f) | X) = (dom (- f)) /\ X by RELAT_1:61 .= (dom f) /\ X by Th5 .= dom (f | X) by RELAT_1:61 .= dom (- (f | X)) by Th5 ; hence (- f) | X = - (f | X) by A2, PARTFUN2:1; ::_thesis: ( (f ^) | X = (f | X) ^ & |.f.| | X = |.(f | X).| ) A9: dom ((f | X) ^) c= dom (f | X) by Th6; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((f_^)_|_X)_holds_ ((f_^)_|_X)_/._c_=_((f_|_X)_^)_/._c let c be Element of C; ::_thesis: ( c in dom ((f ^) | X) implies ((f ^) | X) /. c = ((f | X) ^) /. c ) assume A10: c in dom ((f ^) | X) ; ::_thesis: ((f ^) | X) /. c = ((f | X) ^) /. c then c in (dom (f ^)) /\ X by RELAT_1:61; then A11: c in dom (f ^) by XBOOLE_0:def_4; thus ((f ^) | X) /. c = (f ^) /. c by A10, PARTFUN2:15 .= (f /. c) " by A11, Def2 .= ((f | X) /. c) " by A9, A1, A10, PARTFUN2:15 .= ((f | X) ^) /. c by A1, A10, Def2 ; ::_thesis: verum end; hence (f ^) | X = (f | X) ^ by A1, PARTFUN2:1; ::_thesis: |.f.| | X = |.(f | X).| A12: dom (|.f.| | X) = (dom |.f.|) /\ X by RELAT_1:61 .= (dom f) /\ X by VALUED_1:def_11 .= dom (f | X) by RELAT_1:61 .= dom |.(f | X).| by VALUED_1:def_11 ; now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(|.f.|_|_X)_holds_ (|.f.|_|_X)_._c_=_|.(f_|_X).|_._c let c be Element of C; ::_thesis: ( c in dom (|.f.| | X) implies (|.f.| | X) . c = |.(f | X).| . c ) A13: dom |.f.| = dom f by VALUED_1:def_11; assume A14: c in dom (|.f.| | X) ; ::_thesis: (|.f.| | X) . c = |.(f | X).| . c then A15: c in dom (f | X) by A12, VALUED_1:def_11; c in (dom |.f.|) /\ X by A14, RELAT_1:61; then A16: c in dom |.f.| by XBOOLE_0:def_4; thus (|.f.| | X) . c = |.f.| . c by A14, FUNCT_1:47 .= |.(f . c).| by VALUED_1:18 .= |.(f /. c).| by A16, A13, PARTFUN1:def_6 .= |.((f | X) /. c).| by A15, PARTFUN2:15 .= |.((f | X) . c).| by A15, PARTFUN1:def_6 .= |.(f | X).| . c by VALUED_1:18 ; ::_thesis: verum end; hence |.f.| | X = |.(f | X).| by A12, PARTFUN1:5; ::_thesis: verum end; theorem :: CFUNCT_1:55 for X being set for C being non empty set for f1, f2 being PartFunc of C,COMPLEX 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 C being non empty set for f1, f2 being PartFunc of C,COMPLEX holds ( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) ) let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds ( (f1 - f2) | X = (f1 | X) - (f2 | X) & (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) ) let f1, f2 be PartFunc of C,COMPLEX; ::_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 Th52 .= (f1 | X) - (f2 | X) by Th54 ; ::_thesis: ( (f1 - f2) | X = (f1 | X) - f2 & (f1 - f2) | X = f1 - (f2 | X) ) thus (f1 - f2) | X = (f1 | X) + (- f2) by Th52 .= (f1 | X) - f2 ; ::_thesis: (f1 - f2) | X = f1 - (f2 | X) thus (f1 - f2) | X = f1 + ((- f2) | X) by Th52 .= f1 - (f2 | X) by Th54 ; ::_thesis: verum end; theorem :: CFUNCT_1:56 for X being set for C being non empty set for f1, f2 being PartFunc of C,COMPLEX 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 C being non empty set for f1, f2 being PartFunc of C,COMPLEX holds ( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) ) let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX holds ( (f1 / f2) | X = (f1 | X) / (f2 | X) & (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) ) let f1, f2 be PartFunc of C,COMPLEX; ::_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 Th39 .= (f1 | X) (#) ((f2 ^) | X) by Th53 .= (f1 | X) (#) ((f2 | X) ^) by Th54 .= (f1 | X) / (f2 | X) by Th39 ; ::_thesis: ( (f1 / f2) | X = (f1 | X) / f2 & (f1 / f2) | X = f1 / (f2 | X) ) thus (f1 / f2) | X = (f1 (#) (f2 ^)) | X by Th39 .= (f1 | X) (#) (f2 ^) by Th53 .= (f1 | X) / f2 by Th39 ; ::_thesis: (f1 / f2) | X = f1 / (f2 | X) thus (f1 / f2) | X = (f1 (#) (f2 ^)) | X by Th39 .= f1 (#) ((f2 ^) | X) by Th53 .= f1 (#) ((f2 | X) ^) by Th54 .= f1 / (f2 | X) by Th39 ; ::_thesis: verum end; theorem :: CFUNCT_1:57 for X being set for C being non empty set for f being PartFunc of C,COMPLEX for r being Element of COMPLEX holds (r (#) f) | X = r (#) (f | X) proof let X be set ; ::_thesis: for C being non empty set for f being PartFunc of C,COMPLEX for r being Element of COMPLEX holds (r (#) f) | X = r (#) (f | X) let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX for r being Element of COMPLEX holds (r (#) f) | X = r (#) (f | X) let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds (r (#) f) | X = r (#) (f | X) let r be Element of COMPLEX ; ::_thesis: (r (#) f) | X = r (#) (f | X) A1: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_((r_(#)_f)_|_X)_holds_ ((r_(#)_f)_|_X)_/._c_=_(r_(#)_(f_|_X))_/._c let c be Element of C; ::_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 Th4; 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 Th4; thus ((r (#) f) | X) /. c = (r (#) f) /. c by A2, PARTFUN2:15 .= r * (f /. c) by A5, Th4 .= r * ((f | X) /. c) by A6, PARTFUN2:15 .= (r (#) (f | X)) /. c by A7, Th4 ; ::_thesis: verum end; dom ((r (#) f) | X) = (dom (r (#) f)) /\ X by RELAT_1:61 .= (dom f) /\ X by Th4 .= dom (f | X) by RELAT_1:61 .= dom (r (#) (f | X)) by Th4 ; hence (r (#) f) | X = r (#) (f | X) by A1, PARTFUN2:1; ::_thesis: verum end; begin theorem Th58: :: CFUNCT_1:58 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX 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,COMPLEX 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,COMPLEX; ::_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 ) ) proof assume ( f1 is total & f2 is total ) ; ::_thesis: f1 + f2 is total then ( dom f1 = C & dom f2 = C ) by PARTFUN1:def_2; hence dom (f1 + f2) = C /\ C by VALUED_1:def_1 .= C ; :: according to PARTFUN1:def_2 ::_thesis: verum end; assume f1 + f2 is total ; ::_thesis: ( f1 is total & f2 is total ) then dom (f1 + f2) = C by PARTFUN1:def_2; then (dom f1) /\ (dom f2) = C by VALUED_1:def_1; then ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17; hence ( dom f1 = C & dom f2 = C ) by 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 ) ) proof assume ( f1 is total & f2 is total ) ; ::_thesis: f1 - f2 is total then ( dom f1 = C & dom f2 = C ) by PARTFUN1:def_2; hence dom (f1 - f2) = C /\ C by Th2 .= C ; :: according to PARTFUN1:def_2 ::_thesis: verum end; assume f1 - f2 is total ; ::_thesis: ( f1 is total & f2 is total ) then dom (f1 - f2) = C by PARTFUN1:def_2; then (dom f1) /\ (dom f2) = C by Th2; then ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17; hence ( dom f1 = C & dom f2 = C ) by 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 ) ) proof assume ( f1 is total & f2 is total ) ; ::_thesis: f1 (#) f2 is total then ( dom f1 = C & dom f2 = C ) by PARTFUN1:def_2; hence dom (f1 (#) f2) = C /\ C by Th3 .= C ; :: according to PARTFUN1:def_2 ::_thesis: verum end; assume f1 (#) f2 is total ; ::_thesis: ( f1 is total & f2 is total ) then dom (f1 (#) f2) = C by PARTFUN1:def_2; then (dom f1) /\ (dom f2) = C by Th3; then ( C c= dom f1 & C c= dom f2 ) by XBOOLE_1:17; hence ( dom f1 = C & dom f2 = C ) by XBOOLE_0:def_10; :: according to PARTFUN1:def_2 ::_thesis: verum end; theorem Th59: :: CFUNCT_1:59 for C being non empty set for f being PartFunc of C,COMPLEX for r being Element of COMPLEX holds ( f is total iff r (#) f is total ) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX for r being Element of COMPLEX holds ( f is total iff r (#) f is total ) let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX holds ( f is total iff r (#) f is total ) let r be Element of COMPLEX ; ::_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 ) proof assume f is total ; ::_thesis: r (#) f is total then dom f = C by PARTFUN1:def_2; hence dom (r (#) f) = C by Th4; :: according to PARTFUN1:def_2 ::_thesis: verum end; assume r (#) f is total ; ::_thesis: f is total then dom (r (#) f) = C by PARTFUN1:def_2; hence dom f = C by Th4; :: according to PARTFUN1:def_2 ::_thesis: verum end; theorem Th60: :: CFUNCT_1:60 for C being non empty set for f being PartFunc of C,COMPLEX holds ( f is total iff - f is total ) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds ( f is total iff - f is total ) let f be PartFunc of C,COMPLEX; ::_thesis: ( f is total iff - f is total ) A1: - f = (- 1r) (#) f by COMPLEX1:def_4; thus ( f is total implies - f is total ) ::_thesis: ( - f is total implies f is total ) proof A2: - f = (- 1r) (#) f by COMPLEX1:def_4; assume f is total ; ::_thesis: - f is total hence - f is total by A2, Th59; ::_thesis: verum end; assume - f is total ; ::_thesis: f is total hence f is total by A1, Th59; ::_thesis: verum end; theorem Th61: :: CFUNCT_1:61 for C being non empty set for f being PartFunc of C,COMPLEX holds ( f is total iff |.f.| is total ) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds ( f is total iff |.f.| is total ) let f be PartFunc of C,COMPLEX; ::_thesis: ( f is total iff |.f.| is total ) thus ( f is total implies |.f.| is total ) ::_thesis: ( |.f.| is total implies f is total ) proof assume f is total ; ::_thesis: |.f.| is total then dom f = C by PARTFUN1:def_2; hence dom |.f.| = C by VALUED_1:def_11; :: according to PARTFUN1:def_2 ::_thesis: verum end; assume |.f.| is total ; ::_thesis: f is total then dom |.f.| = C by PARTFUN1:def_2; hence dom f = C by VALUED_1:def_11; :: according to PARTFUN1:def_2 ::_thesis: verum end; theorem Th62: :: CFUNCT_1:62 for C being non empty set for f being PartFunc of C,COMPLEX holds ( f ^ is total iff ( f " {0} = {} & f is total ) ) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds ( f ^ is total iff ( f " {0} = {} & f is total ) ) let f be PartFunc of C,COMPLEX; ::_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 " {0c} c= C ; then f " {0c} c= (dom f) \ (f " {0c}) 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 A2: ( f " {0} = {} & f is total ) ; ::_thesis: f ^ is total thus dom (f ^) = (dom f) \ (f " {0c}) by Def2 .= C by A2, PARTFUN1:def_2 ; :: according to PARTFUN1:def_2 ::_thesis: verum end; theorem Th63: :: CFUNCT_1:63 for C being non empty set for f1, f2 being PartFunc of C,COMPLEX 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,COMPLEX holds ( ( f1 is total & f2 " {0} = {} & f2 is total ) iff f1 / f2 is total ) let f1, f2 be PartFunc of C,COMPLEX; ::_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} = {} & f2 is total ) ; ::_thesis: f1 / f2 is total f2 ^ is total by A2, Th62; then f1 (#) (f2 ^) is total by A1, Th58; hence f1 / f2 is total by Th39; ::_thesis: verum end; assume f1 / f2 is total ; ::_thesis: ( f1 is total & f2 " {0} = {} & f2 is total ) then A3: f1 (#) (f2 ^) is total by Th39; hence f1 is total by Th58; ::_thesis: ( f2 " {0} = {} & f2 is total ) f2 ^ is total by A3, Th58; hence ( f2 " {0} = {} & f2 is total ) by Th62; ::_thesis: verum end; theorem :: CFUNCT_1:64 for C being non empty set for c being Element of C for f1, f2 being PartFunc of C,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_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 A1: ( f1 is total & 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) ) then f1 + f2 is total by Th58; then dom (f1 + f2) = C by PARTFUN1:def_2; hence (f1 + f2) /. c = (f1 /. c) + (f2 /. c) by Th1; ::_thesis: ( (f1 - f2) /. c = (f1 /. c) - (f2 /. c) & (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ) f1 - f2 is total by A1, Th58; then dom (f1 - f2) = C by PARTFUN1:def_2; hence (f1 - f2) /. c = (f1 /. c) - (f2 /. c) by Th2; ::_thesis: (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) f1 (#) f2 is total by A1, Th58; then dom (f1 (#) f2) = C by PARTFUN1:def_2; hence (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) by Th3; ::_thesis: verum end; theorem :: CFUNCT_1:65 for C being non empty set for c being Element of C for f being PartFunc of C,COMPLEX for r being Element of COMPLEX 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 f being PartFunc of C,COMPLEX for r being Element of COMPLEX st f is total holds (r (#) f) /. c = r * (f /. c) let c be Element of C; ::_thesis: for f being PartFunc of C,COMPLEX for r being Element of COMPLEX st f is total holds (r (#) f) /. c = r * (f /. c) let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX st f is total holds (r (#) f) /. c = r * (f /. c) let r be Element of COMPLEX ; ::_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 by Th59; then dom (r (#) f) = C by PARTFUN1:def_2; hence (r (#) f) /. c = r * (f /. c) by Th4; ::_thesis: verum end; theorem :: CFUNCT_1:66 for C being non empty set for c being Element of C for f being PartFunc of C,COMPLEX st f is total holds ( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| ) proof let C be non empty set ; ::_thesis: for c being Element of C for f being PartFunc of C,COMPLEX st f is total holds ( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| ) let c be Element of C; ::_thesis: for f being PartFunc of C,COMPLEX st f is total holds ( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| ) let f be PartFunc of C,COMPLEX; ::_thesis: ( f is total implies ( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| ) ) assume A1: f is total ; ::_thesis: ( (- f) /. c = - (f /. c) & |.f.| . c = |.(f /. c).| ) then |.f.| is total by Th61; then A2: ( dom |.f.| = dom f & dom |.f.| = C ) by PARTFUN1:def_2, VALUED_1:def_11; - f is total by A1, Th60; then dom (- f) = C by PARTFUN1:def_2; hence (- f) /. c = - (f /. c) by Th5; ::_thesis: |.f.| . c = |.(f /. c).| thus |.f.| . c = |.(f . c).| by VALUED_1:18 .= |.(f /. c).| by A2, PARTFUN1:def_6 ; ::_thesis: verum end; theorem :: CFUNCT_1:67 for C being non empty set for c being Element of C for f being PartFunc of C,COMPLEX 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,COMPLEX st f ^ is total holds (f ^) /. c = (f /. c) " let c be Element of C; ::_thesis: for f being PartFunc of C,COMPLEX st f ^ is total holds (f ^) /. c = (f /. c) " let f be PartFunc of C,COMPLEX; ::_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 :: CFUNCT_1:68 for C being non empty set for c being Element of C for f1, f2 being PartFunc of C,COMPLEX 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,COMPLEX 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,COMPLEX st f1 is total & f2 ^ is total holds (f1 / f2) /. c = (f1 /. c) * ((f2 /. c) ") let f1, f2 be PartFunc of C,COMPLEX; ::_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) ") ( f2 " {0c} = {} & f2 is total ) by A2, Th62; then f1 / f2 is total by A1, Th63; then dom (f1 / f2) = C by PARTFUN1:def_2; hence (f1 / f2) /. c = (f1 /. c) * ((f2 /. c) ") by Def1; ::_thesis: verum end; begin Lm3: for C being non empty set for f being PartFunc of C,COMPLEX holds ( |.f.| is bounded iff f is bounded ) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds ( |.f.| is bounded iff f is bounded ) let f be PartFunc of C,COMPLEX; ::_thesis: ( |.f.| is bounded iff f is bounded ) A1: dom f = dom |.f.| by VALUED_1:def_11; thus ( |.f.| is bounded implies f is bounded ) ::_thesis: ( f is bounded implies |.f.| is bounded ) proof assume |.f.| is bounded ; ::_thesis: f is bounded then consider r1 being real number such that A2: for y being set st y in dom |.f.| holds abs (|.f.| . y) < r1 by COMSEQ_2:def_3; take r1 ; :: according to COMSEQ_2:def_3 ::_thesis: for b1 being set holds ( not b1 in K104(f) or not r1 <= abs (f . b1) ) let y be set ; ::_thesis: ( not y in K104(f) or not r1 <= abs (f . y) ) assume A3: y in dom f ; ::_thesis: not r1 <= abs (f . y) then abs (|.f.| . y) < r1 by A1, A2; then abs |.(f . y).| < r1 by A1, A3, VALUED_1:def_11; hence not r1 <= abs (f . y) ; ::_thesis: verum end; given r1 being real number such that A4: for y being set st y in dom f holds abs (f . y) < r1 ; :: according to COMSEQ_2:def_3 ::_thesis: |.f.| is bounded now__::_thesis:_ex_r1_being_real_number_st_ for_y_being_set_st_y_in_dom_|.f.|_holds_ abs_(|.f.|_._y)_<_r1 take r1 = r1; ::_thesis: for y being set st y in dom |.f.| holds abs (|.f.| . y) < r1 let y be set ; ::_thesis: ( y in dom |.f.| implies abs (|.f.| . y) < r1 ) assume A5: y in dom |.f.| ; ::_thesis: abs (|.f.| . y) < r1 then abs |.(f . y).| < r1 by A1, A4; hence abs (|.f.| . y) < r1 by A5, VALUED_1:def_11; ::_thesis: verum end; hence |.f.| is bounded by COMSEQ_2:def_3; ::_thesis: verum end; theorem Th69: :: CFUNCT_1:69 for Y being set for C being non empty set for f being PartFunc of C,COMPLEX holds ( f | Y is bounded iff ex p being real number st for c being Element of C st c in Y /\ (dom f) holds |.(f /. c).| <= p ) proof let Y be set ; ::_thesis: for C being non empty set for f being PartFunc of C,COMPLEX holds ( f | Y is bounded iff ex p being real number st for c being Element of C st c in Y /\ (dom f) holds |.(f /. c).| <= p ) let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds ( f | Y is bounded iff ex p being real number st for c being Element of C st c in Y /\ (dom f) holds |.(f /. c).| <= p ) let f be PartFunc of C,COMPLEX; ::_thesis: ( f | Y is bounded iff ex p being real number st for c being Element of C st c in Y /\ (dom f) holds |.(f /. c).| <= p ) A1: dom |.f.| = dom f by VALUED_1:def_11; A2: dom (|.f.| | Y) = Y /\ (dom |.f.|) by RELAT_1:61; A3: |.f.| | Y = |.(f | Y).| by RFUNCT_1:46; hereby ::_thesis: ( ex p being real number st for c being Element of C st c in Y /\ (dom f) holds |.(f /. c).| <= p implies f | Y is bounded ) assume f | Y is bounded ; ::_thesis: ex p being real number st for c being Element of C st c in Y /\ (dom f) holds |.(f /. c).| <= p then |.f.| | Y is bounded by A3, Lm3; then consider p being real number such that A4: for c being set st c in dom (|.f.| | Y) holds abs ((|.f.| | Y) . c) <= p by RFUNCT_1:72; now__::_thesis:_for_c_being_Element_of_C_st_c_in_Y_/\_(dom_f)_holds_ |.(f_/._c).|_<=_p let c be Element of C; ::_thesis: ( c in Y /\ (dom f) implies |.(f /. c).| <= p ) assume A5: c in Y /\ (dom f) ; ::_thesis: |.(f /. c).| <= p c in dom f by A5, XBOOLE_0:def_4; then A6: f . c = f /. c by PARTFUN1:def_6; abs ((|.f.| | Y) . c) = abs (|.f.| . c) by A1, A2, A5, FUNCT_1:47 .= abs |.(f . c).| by VALUED_1:18 ; hence |.(f /. c).| <= p by A1, A2, A4, A5, A6; ::_thesis: verum end; hence ex p being real number st for c being Element of C st c in Y /\ (dom f) holds |.(f /. c).| <= p ; ::_thesis: verum end; given p being real number such that A7: for c being Element of C st c in Y /\ (dom f) holds |.(f /. c).| <= p ; ::_thesis: f | Y is bounded A8: dom |.f.| = dom f by VALUED_1:def_11; now__::_thesis:_for_c_being_set_st_c_in_dom_(|.f.|_|_Y)_holds_ abs_((|.f.|_|_Y)_._c)_<=_p let c be set ; ::_thesis: ( c in dom (|.f.| | Y) implies abs ((|.f.| | Y) . c) <= p ) assume A9: c in dom (|.f.| | Y) ; ::_thesis: abs ((|.f.| | Y) . c) <= p A10: c in dom |.f.| by A9, RELAT_1:57; abs ((|.f.| | Y) . c) = abs (|.f.| . c) by A9, FUNCT_1:47 .= abs |.(f . c).| by VALUED_1:18 .= abs |.(f /. c).| by A1, A10, PARTFUN1:def_6 ; hence abs ((|.f.| | Y) . c) <= p by A2, A7, A8, A9; ::_thesis: verum end; then |.f.| | Y is bounded by RFUNCT_1:72; hence f | Y is bounded by A3, Lm3; ::_thesis: verum end; theorem :: CFUNCT_1:70 for Y, X being set for C being non empty set for f being PartFunc of C,COMPLEX st Y c= X & f | X is bounded holds f | Y is bounded proof let Y, X be set ; ::_thesis: for C being non empty set for f being PartFunc of C,COMPLEX st Y c= X & f | X is bounded holds f | Y is bounded let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX st Y c= X & f | X is bounded holds f | Y is bounded let f be PartFunc of C,COMPLEX; ::_thesis: ( Y c= X & f | X is bounded implies f | Y is bounded ) assume that A1: Y c= X and A2: f | X is bounded ; ::_thesis: f | Y is bounded |.f.| | X = |.(f | X).| by RFUNCT_1:46; then |.f.| | X is bounded by A2, Lm3; then ( |.f.| | Y = |.(f | Y).| & |.f.| | Y is bounded ) by A1, RFUNCT_1:46, RFUNCT_1:74; hence f | Y is bounded by Lm3; ::_thesis: verum end; theorem :: CFUNCT_1:71 for X being set for C being non empty set for f being PartFunc of C,COMPLEX st X misses dom f holds f | X is bounded proof let X be set ; ::_thesis: for C being non empty set for f being PartFunc of C,COMPLEX st X misses dom f holds f | X is bounded let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX st X misses dom f holds f | X is bounded let f be PartFunc of C,COMPLEX; ::_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 for c being Element of C st c in X /\ (dom f) holds |.(f /. c).| <= 0 ; hence f | X is bounded by Th69; ::_thesis: verum end; theorem Th72: :: CFUNCT_1:72 for Y being set for C being non empty set for f being PartFunc of C,COMPLEX for r being Element of COMPLEX st f | Y is bounded holds (r (#) f) | Y is bounded proof let Y be set ; ::_thesis: for C being non empty set for f being PartFunc of C,COMPLEX for r being Element of COMPLEX st f | Y is bounded holds (r (#) f) | Y is bounded let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX for r being Element of COMPLEX st f | Y is bounded holds (r (#) f) | Y is bounded let f be PartFunc of C,COMPLEX; ::_thesis: for r being Element of COMPLEX st f | Y is bounded holds (r (#) f) | Y is bounded let r be Element of COMPLEX ; ::_thesis: ( f | Y is bounded implies (r (#) f) | Y is bounded ) assume A1: f | Y is bounded ; ::_thesis: (r (#) f) | Y is bounded |.f.| | Y = |.(f | Y).| by RFUNCT_1:46; then |.f.| | Y is bounded by A1, Lm3; then (|.r.| (#) |.f.|) | Y is bounded by RFUNCT_1:80; then ( |.(r (#) f).| | Y = |.((r (#) f) | Y).| & |.(r (#) f).| | Y is bounded ) by Th30, RFUNCT_1:46; hence (r (#) f) | Y is bounded by Lm3; ::_thesis: verum end; theorem :: CFUNCT_1:73 for X being set for C being non empty set for f being PartFunc of C,COMPLEX holds |.f.| | X is bounded_below proof let X be set ; ::_thesis: for C being non empty set for f being PartFunc of C,COMPLEX holds |.f.| | X is bounded_below let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX holds |.f.| | X is bounded_below let f be PartFunc of C,COMPLEX; ::_thesis: |.f.| | X is bounded_below now__::_thesis:_ex_z_being_Element_of_NAT_st_ for_c_being_set_st_c_in_X_/\_(dom_|.f.|)_holds_ z_<=_|.f.|_._c take z = 0 ; ::_thesis: for c being set st c in X /\ (dom |.f.|) holds z <= |.f.| . c let c be set ; ::_thesis: ( c in X /\ (dom |.f.|) implies z <= |.f.| . c ) A1: z <= |.(f /. c).| by COMPLEX1:46; assume c in X /\ (dom |.f.|) ; ::_thesis: z <= |.f.| . c then A2: c in dom |.f.| by XBOOLE_0:def_4; dom |.f.| = dom f by VALUED_1:def_11; then f . c = f /. c by A2, PARTFUN1:def_6; hence z <= |.f.| . c by A1, VALUED_1:18; ::_thesis: verum end; hence |.f.| | X is bounded_below by RFUNCT_1:71; ::_thesis: verum end; theorem Th74: :: CFUNCT_1:74 for Y being set for C being non empty set for f being PartFunc of C,COMPLEX st f | Y is bounded holds ( |.f.| | Y is bounded & (- f) | Y is bounded ) proof let Y be set ; ::_thesis: for C being non empty set for f being PartFunc of C,COMPLEX st f | Y is bounded holds ( |.f.| | Y is bounded & (- f) | Y is bounded ) let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX st f | Y is bounded holds ( |.f.| | Y is bounded & (- f) | Y is bounded ) let f be PartFunc of C,COMPLEX; ::_thesis: ( f | Y is bounded implies ( |.f.| | Y is bounded & (- f) | Y is bounded ) ) assume A1: f | Y is bounded ; ::_thesis: ( |.f.| | Y is bounded & (- f) | Y is bounded ) |.f.| | Y = |.(f | Y).| by RFUNCT_1:46; hence |.f.| | Y is bounded by A1, Lm3; ::_thesis: (- f) | Y is bounded (- 1r) (#) (f | Y) = ((- 1r) (#) f) | Y by RFUNCT_1:49; hence (- f) | Y is bounded by A1, Th72, COMPLEX1:def_4; ::_thesis: verum end; theorem Th75: :: CFUNCT_1:75 for X, Y being set for C being non empty set for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is bounded holds (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,COMPLEX st f1 | X is bounded & f2 | Y is bounded holds (f1 + f2) | (X /\ Y) is bounded let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is bounded holds (f1 + f2) | (X /\ Y) is bounded let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( f1 | X is bounded & f2 | Y is bounded implies (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 consider r1 being real number such that A3: for c being Element of C st c in X /\ (dom f1) holds |.(f1 /. c).| <= r1 by A1, Th69; consider r2 being real number such that A4: for c being Element of C st c in Y /\ (dom f2) holds |.(f2 /. c).| <= r2 by A2, Th69; ex p1 being real number st for c being Element of C st c in (X /\ Y) /\ (dom (f1 + f2)) holds |.((f1 + f2) /. c).| <= p1 proof take r0 = r1 + r2; ::_thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 + f2)) holds |.((f1 + f2) /. c).| <= r0 let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies |.((f1 + f2) /. c).| <= r0 ) A5: |.((f1 /. c) + (f2 /. c)).| <= |.(f1 /. c).| + |.(f2 /. c).| by COMPLEX1:56; assume A6: c in (X /\ Y) /\ (dom (f1 + f2)) ; ::_thesis: |.((f1 + f2) /. c).| <= r0 then A7: c in X /\ Y by XBOOLE_0:def_4; then A8: c in X by XBOOLE_0:def_4; A9: c in Y by A7, XBOOLE_0:def_4; A10: c in dom (f1 + f2) by A6, XBOOLE_0:def_4; then A11: c in (dom f1) /\ (dom f2) by VALUED_1:def_1; then c in dom f2 by XBOOLE_0:def_4; then c in Y /\ (dom f2) by A9, XBOOLE_0:def_4; then A12: |.(f2 /. c).| <= r2 by A4; c in dom f1 by A11, XBOOLE_0:def_4; then c in X /\ (dom f1) by A8, XBOOLE_0:def_4; then |.(f1 /. c).| <= r1 by A3; then |.(f1 /. c).| + |.(f2 /. c).| <= r0 by A12, XREAL_1:7; then |.((f1 /. c) + (f2 /. c)).| <= r0 by A5, XXREAL_0:2; hence |.((f1 + f2) /. c).| <= r0 by A10, Th1; ::_thesis: verum end; hence (f1 + f2) | (X /\ Y) is bounded by Th69; ::_thesis: verum end; theorem Th76: :: CFUNCT_1:76 for X, Y being set for C being non empty set for f1, f2 being PartFunc of C,COMPLEX 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 C being non empty set for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is bounded holds ( (f1 (#) f2) | (X /\ Y) is bounded & (f1 - f2) | (X /\ Y) is bounded ) let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX 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 PartFunc of C,COMPLEX; ::_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 ) consider r1 being real number such that A3: for c being Element of C st c in X /\ (dom f1) holds |.(f1 /. c).| <= r1 by A1, Th69; consider r2 being real number such that A4: for c being Element of C st c in Y /\ (dom f2) holds |.(f2 /. c).| <= r2 by A2, Th69; now__::_thesis:_ex_r_being_set_st_ for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_(#)_f2))_holds_ |.((f1_(#)_f2)_/._c).|_<=_r take r = r1 * r2; ::_thesis: for c being Element of C st c in (X /\ Y) /\ (dom (f1 (#) f2)) holds |.((f1 (#) f2) /. c).| <= r let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies |.((f1 (#) f2) /. c).| <= r ) assume A5: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; ::_thesis: |.((f1 (#) f2) /. c).| <= r 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 Th3; then c in dom f1 by XBOOLE_0:def_4; then c in X /\ (dom f1) by A7, XBOOLE_0:def_4; then A10: |.(f1 /. c).| <= r1 by A3; A11: c in Y by A6, XBOOLE_0:def_4; c in dom f2 by A9, XBOOLE_0:def_4; then c in Y /\ (dom f2) by A11, XBOOLE_0:def_4; then A12: |.(f2 /. c).| <= r2 by A4; ( 0 <= |.(f1 /. c).| & 0 <= |.(f2 /. c).| ) by COMPLEX1:46; then |.(f1 /. c).| * |.(f2 /. c).| <= r by A10, A12, XREAL_1:66; then |.((f1 /. c) * (f2 /. c)).| <= r by COMPLEX1:65; hence |.((f1 (#) f2) /. c).| <= r by A8, Th3; ::_thesis: verum end; hence (f1 (#) f2) | (X /\ Y) is bounded by Th69; ::_thesis: (f1 - f2) | (X /\ Y) is bounded (- f2) | Y is bounded by A2, Th74; hence (f1 - f2) | (X /\ Y) is bounded by A1, Th75; ::_thesis: verum end; theorem :: CFUNCT_1:77 for X, Y being set for C being non empty set for f being PartFunc of C,COMPLEX st f | X is bounded & f | Y is bounded holds f | (X \/ Y) is bounded proof let X, Y be set ; ::_thesis: for C being non empty set for f being PartFunc of C,COMPLEX st f | X is bounded & f | Y is bounded holds f | (X \/ Y) is bounded let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX st f | X is bounded & f | Y is bounded holds f | (X \/ Y) is bounded let f be PartFunc of C,COMPLEX; ::_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 |.f.| | Y = |.(f | Y).| by RFUNCT_1:46; then A3: |.f.| | Y is bounded by A2, Lm3; |.f.| | X = |.(f | X).| by RFUNCT_1:46; then |.f.| | X is bounded by A1, Lm3; then ( |.f.| | (X \/ Y) = |.(f | (X \/ Y)).| & |.f.| | (X \/ Y) is bounded ) by A3, RFUNCT_1:46, RFUNCT_1:87; hence f | (X \/ Y) is bounded by Lm3; ::_thesis: verum end; theorem :: CFUNCT_1:78 for X, Y being set for C being non empty set for f1, f2 being PartFunc of C,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_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 cr1 being Element of COMPLEX such that A3: for c being Element of C st c in X /\ (dom f1) holds f1 /. c = cr1 by A1, PARTFUN2:35; consider cr2 being Element of COMPLEX such that A4: for c being Element of C st c in Y /\ (dom f2) holds f2 /. c = cr2 by A2, PARTFUN2:35; now__::_thesis:_for_c_being_Element_of_C_st_c_in_(X_/\_Y)_/\_(dom_(f1_+_f2))_holds_ (f1_+_f2)_/._c_=_cr1_+_cr2 let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 + f2)) implies (f1 + f2) /. c = cr1 + cr2 ) assume A5: c in (X /\ Y) /\ (dom (f1 + f2)) ; ::_thesis: (f1 + f2) /. c = cr1 + cr2 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, Th1 .= cr1 + (f2 /. c) by A3, A10 .= cr1 + cr2 by A4, A12 ; ::_thesis: verum end; hence (f1 + f2) | (X /\ Y) is constant by PARTFUN2:35; ::_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_=_cr1_-_cr2 let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 - f2)) implies (f1 - f2) /. c = cr1 - cr2 ) assume A13: c in (X /\ Y) /\ (dom (f1 - f2)) ; ::_thesis: (f1 - f2) /. c = cr1 - cr2 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 Th2; 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, Th2 .= cr1 - (f2 /. c) by A3, A18 .= cr1 - cr2 by A4, A20 ; ::_thesis: verum end; hence (f1 - f2) | (X /\ Y) is constant by PARTFUN2:35; ::_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_=_cr1_*_cr2 let c be Element of C; ::_thesis: ( c in (X /\ Y) /\ (dom (f1 (#) f2)) implies (f1 (#) f2) /. c = cr1 * cr2 ) assume A21: c in (X /\ Y) /\ (dom (f1 (#) f2)) ; ::_thesis: (f1 (#) f2) /. c = cr1 * cr2 then A22: c in X /\ Y by XBOOLE_0:def_4; then A23: c in X by XBOOLE_0:def_4; A24: c in dom (f1 (#) f2) by A21, XBOOLE_0:def_4; then A25: c in (dom f1) /\ (dom f2) by Th3; then c in dom f1 by XBOOLE_0:def_4; then A26: c in X /\ (dom f1) by A23, XBOOLE_0:def_4; A27: c in Y by A22, XBOOLE_0:def_4; c in dom f2 by A25, XBOOLE_0:def_4; then A28: c in Y /\ (dom f2) by A27, XBOOLE_0:def_4; thus (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) by A24, Th3 .= cr1 * (f2 /. c) by A3, A26 .= cr1 * cr2 by A4, A28 ; ::_thesis: verum end; hence (f1 (#) f2) | (X /\ Y) is constant by PARTFUN2:35; ::_thesis: verum end; theorem Th79: :: CFUNCT_1:79 for Y being set for C being non empty set for f being PartFunc of C,COMPLEX for q being Element of COMPLEX st f | Y is constant holds (q (#) f) | Y is constant proof let Y be set ; ::_thesis: for C being non empty set for f being PartFunc of C,COMPLEX for q being Element of COMPLEX st f | Y is constant holds (q (#) f) | Y is constant let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX for q being Element of COMPLEX st f | Y is constant holds (q (#) f) | Y is constant let f be PartFunc of C,COMPLEX; ::_thesis: for q being Element of COMPLEX st f | Y is constant holds (q (#) f) | Y is constant let q be Element of COMPLEX ; ::_thesis: ( f | Y is constant implies (q (#) f) | Y is constant ) assume f | Y is constant ; ::_thesis: (q (#) f) | Y is constant then consider r being Element of COMPLEX such that A1: for c being Element of C st c in Y /\ (dom f) holds f /. c = r by PARTFUN2:35; now__::_thesis:_for_c_being_Element_of_C_st_c_in_Y_/\_(dom_(q_(#)_f))_holds_ (q_(#)_f)_/._c_=_q_*_r let c be Element of C; ::_thesis: ( c in Y /\ (dom (q (#) f)) implies (q (#) f) /. c = q * r ) assume A2: c in Y /\ (dom (q (#) f)) ; ::_thesis: (q (#) f) /. c = q * r then A3: c in Y by XBOOLE_0:def_4; A4: c in dom (q (#) f) by A2, XBOOLE_0:def_4; then c in dom f by Th4; then A5: c in Y /\ (dom f) by A3, XBOOLE_0:def_4; thus (q (#) f) /. c = q * (f /. c) by A4, Th4 .= q * r by A1, A5 ; ::_thesis: verum end; hence (q (#) f) | Y is constant by PARTFUN2:35; ::_thesis: verum end; theorem Th80: :: CFUNCT_1:80 for Y being set for C being non empty set for f being PartFunc of C,COMPLEX st f | Y is constant holds ( |.f.| | Y is constant & (- f) | Y is constant ) proof let Y be set ; ::_thesis: for C being non empty set for f being PartFunc of C,COMPLEX st f | Y is constant holds ( |.f.| | Y is constant & (- f) | Y is constant ) let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX st f | Y is constant holds ( |.f.| | Y is constant & (- f) | Y is constant ) let f be PartFunc of C,COMPLEX; ::_thesis: ( f | Y is constant implies ( |.f.| | Y is constant & (- f) | Y is constant ) ) assume f | Y is constant ; ::_thesis: ( |.f.| | Y is constant & (- f) | Y is constant ) then consider r being Element of COMPLEX such that A1: for c being Element of C st c in Y /\ (dom f) holds f /. c = r by PARTFUN2:35; now__::_thesis:_for_c_being_Element_of_C_st_c_in_Y_/\_(dom_|.f.|)_holds_ |.f.|_._c_=_|.r.| let c be Element of C; ::_thesis: ( c in Y /\ (dom |.f.|) implies |.f.| . c = |.r.| ) assume A2: c in Y /\ (dom |.f.|) ; ::_thesis: |.f.| . c = |.r.| then c in dom |.f.| by XBOOLE_0:def_4; then A3: c in dom f by VALUED_1:def_11; c in Y by A2, XBOOLE_0:def_4; then A4: c in Y /\ (dom f) by A3, XBOOLE_0:def_4; f . c = f /. c by A3, PARTFUN1:def_6; hence |.f.| . c = |.(f /. c).| by VALUED_1:18 .= |.r.| by A1, A4 ; ::_thesis: verum end; hence |.f.| | Y is constant by PARTFUN2:57; ::_thesis: (- f) | Y is constant now__::_thesis:_ex_p_being_Element_of_COMPLEX_st_ for_c_being_Element_of_C_st_c_in_Y_/\_(dom_(-_f))_holds_ (-_f)_/._c_=_p take p = - r; ::_thesis: for c being Element of C st c in Y /\ (dom (- f)) holds (- f) /. c = p let c be Element of C; ::_thesis: ( c in Y /\ (dom (- f)) implies (- f) /. c = p ) assume A5: c in Y /\ (dom (- f)) ; ::_thesis: (- f) /. c = p then c in Y /\ (dom f) by Th5; then A6: - (f /. c) = p by A1; c in dom (- f) by A5, XBOOLE_0:def_4; hence (- f) /. c = p by A6, Th5; ::_thesis: verum end; hence (- f) | Y is constant by PARTFUN2:35; ::_thesis: verum end; theorem Th81: :: CFUNCT_1:81 for Y being set for C being non empty set for f being PartFunc of C,COMPLEX st f | Y is constant holds f | Y is bounded proof let Y be set ; ::_thesis: for C being non empty set for f being PartFunc of C,COMPLEX st f | Y is constant holds f | Y is bounded let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX st f | Y is constant holds f | Y is bounded let f be PartFunc of C,COMPLEX; ::_thesis: ( f | Y is constant implies f | Y is bounded ) assume f | Y is constant ; ::_thesis: f | Y is bounded then consider r being Element of COMPLEX such that A1: for c being Element of C st c in Y /\ (dom f) holds f /. c = r by PARTFUN2:35; now__::_thesis:_ex_p_being_Element_of_REAL_st_ for_c_being_Element_of_C_st_c_in_Y_/\_(dom_f)_holds_ |.(f_/._c).|_<=_p take p = |.r.|; ::_thesis: for c being Element of C st c in Y /\ (dom f) holds |.(f /. c).| <= p let c be Element of C; ::_thesis: ( c in Y /\ (dom f) implies |.(f /. c).| <= p ) assume c in Y /\ (dom f) ; ::_thesis: |.(f /. c).| <= p hence |.(f /. c).| <= p by A1; ::_thesis: verum end; hence f | Y is bounded by Th69; ::_thesis: verum end; theorem :: CFUNCT_1:82 for Y being set for C being non empty set for f being PartFunc of C,COMPLEX st f | Y is constant holds ( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded ) proof let Y be set ; ::_thesis: for C being non empty set for f being PartFunc of C,COMPLEX st f | Y is constant holds ( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded ) let C be non empty set ; ::_thesis: for f being PartFunc of C,COMPLEX st f | Y is constant holds ( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded ) let f be PartFunc of C,COMPLEX; ::_thesis: ( f | Y is constant implies ( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded ) ) assume A1: f | Y is constant ; ::_thesis: ( ( for r being Element of COMPLEX holds (r (#) f) | Y is bounded ) & (- f) | Y is bounded & |.f.| | Y is bounded ) hence for r being Element of COMPLEX holds (r (#) f) | Y is bounded by Th79, Th81; ::_thesis: ( (- f) | Y is bounded & |.f.| | Y is bounded ) thus (- f) | Y is bounded by A1, Th80, Th81; ::_thesis: |.f.| | Y is bounded |.f.| | Y is constant by A1, Th80; hence |.f.| | Y is bounded ; ::_thesis: verum end; theorem Th83: :: CFUNCT_1:83 for X, Y being set for C being non empty set for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is constant holds (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,COMPLEX st f1 | X is bounded & f2 | Y is constant holds (f1 + f2) | (X /\ Y) is bounded let C be non empty set ; ::_thesis: for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is constant holds (f1 + f2) | (X /\ Y) is bounded let f1, f2 be PartFunc of C,COMPLEX; ::_thesis: ( f1 | X is bounded & f2 | Y is constant implies (f1 + f2) | (X /\ Y) is bounded ) assume that A1: f1 | X is bounded and A2: f2 | Y is constant ; ::_thesis: (f1 + f2) | (X /\ Y) is bounded f2 | Y is bounded by A2, Th81; hence (f1 + f2) | (X /\ Y) is bounded by A1, Th75; ::_thesis: verum end; theorem :: CFUNCT_1:84 for X, Y being set for C being non empty set for f1, f2 being PartFunc of C,COMPLEX st f1 | X is bounded & f2 | Y is constant holds ( (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,COMPLEX st f1 | X is bounded & f2 | Y is constant holds ( (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,COMPLEX st f1 | X is bounded & f2 | Y is constant holds ( (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,COMPLEX; ::_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 ) ) assume that A1: f1 | X is bounded and A2: 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 A2, Th80; hence (f1 - f2) | (X /\ Y) is bounded by A1, Th83; ::_thesis: ( (f2 - f1) | (X /\ Y) is bounded & (f1 (#) f2) | (X /\ Y) is bounded ) A3: f2 | Y is bounded by A2, Th81; hence (f2 - f1) | (X /\ Y) is bounded by A1, Th76; ::_thesis: (f1 (#) f2) | (X /\ Y) is bounded thus (f1 (#) f2) | (X /\ Y) is bounded by A1, A3, Th76; ::_thesis: verum end; theorem :: CFUNCT_1:85 for C being non empty set for f being PartFunc of C,COMPLEX holds ( |.f.| is bounded iff f is bounded ) by Lm3;