:: INTEGR16 semantic presentation begin theorem Th1: :: INTEGR16:1 for z being complex number for r being real number holds ( Re (r * z) = r * (Re z) & Im (r * z) = r * (Im z) ) proof let z be complex number ; ::_thesis: for r being real number holds ( Re (r * z) = r * (Re z) & Im (r * z) = r * (Im z) ) let r be real number ; ::_thesis: ( Re (r * z) = r * (Re z) & Im (r * z) = r * (Im z) ) A1: r in REAL by XREAL_0:def_1; then A2: Re r = r by COMPLEX1:def_1; hence Re (r * z) = (r * (Re z)) - ((Im r) * (Im z)) by COMPLEX1:9 .= (r * (Re z)) - (0 * (Im z)) by A1, COMPLEX1:def_2 .= r * (Re z) ; ::_thesis: Im (r * z) = r * (Im z) thus Im (r * z) = (r * (Im z)) + ((Re z) * (Im r)) by A2, COMPLEX1:9 .= (r * (Im z)) + (0 * (Re z)) by A1, COMPLEX1:def_2 .= r * (Im z) ; ::_thesis: verum end; Lm1: now__::_thesis:_for_f_being_FinSequence for_g_being_Function_st_dom_f_=_dom_g_holds_ g_is_FinSequence let f be FinSequence; ::_thesis: for g being Function st dom f = dom g holds g is FinSequence let g be Function; ::_thesis: ( dom f = dom g implies g is FinSequence ) ex n being Nat st dom f = Seg n by FINSEQ_1:def_2; hence ( dom f = dom g implies g is FinSequence ) by FINSEQ_1:def_2; ::_thesis: verum end; registration let S be FinSequence of COMPLEX ; cluster Re S -> FinSequence-like ; coherence Re S is FinSequence-like proof dom (Re S) = dom S by COMSEQ_3:def_3; hence Re S is FinSequence-like by Lm1; ::_thesis: verum end; cluster Im S -> FinSequence-like ; coherence Im S is FinSequence-like proof dom (Im S) = dom S by COMSEQ_3:def_4; hence Im S is FinSequence-like by Lm1; ::_thesis: verum end; end; definition let S be FinSequence of COMPLEX ; :: original: Re redefine func Re S -> FinSequence of REAL ; coherence Re S is FinSequence of REAL proof rng (Re S) c= REAL ; hence Re S is FinSequence of REAL by FINSEQ_1:def_4; ::_thesis: verum end; :: original: Im redefine func Im S -> FinSequence of REAL ; coherence Im S is FinSequence of REAL proof rng (Im S) c= REAL ; hence Im S is FinSequence of REAL by FINSEQ_1:def_4; ::_thesis: verum end; end; definition let A be non empty closed_interval Subset of REAL; let f be Function of A,COMPLEX; let D be Division of A; mode middle_volume of f,D -> FinSequence of COMPLEX means :Def1: :: INTEGR16:def 1 ( len it = len D & ( for i being Nat st i in dom D holds ex c being Element of COMPLEX st ( c in rng (f | (divset (D,i))) & it . i = c * (vol (divset (D,i))) ) ) ); correctness existence ex b1 being FinSequence of COMPLEX st ( len b1 = len D & ( for i being Nat st i in dom D holds ex c being Element of COMPLEX st ( c in rng (f | (divset (D,i))) & b1 . i = c * (vol (divset (D,i))) ) ) ); proof defpred S1[ Nat, set ] means ex c being Element of COMPLEX st ( c in rng (f | (divset (D,\$1))) & \$2 = c * (vol (divset (D,\$1))) ); A1: Seg (len D) = dom D by FINSEQ_1:def_3; A2: for k being Nat st k in Seg (len D) holds ex x being Element of COMPLEX st S1[k,x] proof let k be Nat; ::_thesis: ( k in Seg (len D) implies ex x being Element of COMPLEX st S1[k,x] ) assume k in Seg (len D) ; ::_thesis: ex x being Element of COMPLEX st S1[k,x] then A3: k in dom D by FINSEQ_1:def_3; dom f = A by FUNCT_2:def_1; then dom (f | (divset (D,k))) = divset (D,k) by A3, INTEGRA1:8, RELAT_1:62; then not rng (f | (divset (D,k))) is empty by RELAT_1:42; then consider c being set such that A4: c in rng (f | (divset (D,k))) by XBOOLE_0:def_1; reconsider c = c as Element of COMPLEX by A4; c * (vol (divset (D,k))) is Element of COMPLEX ; hence ex x being Element of COMPLEX st S1[k,x] by A4; ::_thesis: verum end; consider p being FinSequence of COMPLEX such that A5: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds S1[k,p . k] ) ) from FINSEQ_1:sch_5(A2); len p = len D by A5, FINSEQ_1:def_3; hence ex b1 being FinSequence of COMPLEX st ( len b1 = len D & ( for i being Nat st i in dom D holds ex c being Element of COMPLEX st ( c in rng (f | (divset (D,i))) & b1 . i = c * (vol (divset (D,i))) ) ) ) by A5, A1; ::_thesis: verum end; end; :: deftheorem Def1 defines middle_volume INTEGR16:def_1_:_ for A being non empty closed_interval Subset of REAL for f being Function of A,COMPLEX for D being Division of A for b4 being FinSequence of COMPLEX holds ( b4 is middle_volume of f,D iff ( len b4 = len D & ( for i being Nat st i in dom D holds ex c being Element of COMPLEX st ( c in rng (f | (divset (D,i))) & b4 . i = c * (vol (divset (D,i))) ) ) ) ); definition let A be non empty closed_interval Subset of REAL; let f be Function of A,COMPLEX; let D be Division of A; let F be middle_volume of f,D; func middle_sum (f,F) -> Element of COMPLEX equals :: INTEGR16:def 2 Sum F; coherence Sum F is Element of COMPLEX ; end; :: deftheorem defines middle_sum INTEGR16:def_2_:_ for A being non empty closed_interval Subset of REAL for f being Function of A,COMPLEX for D being Division of A for F being middle_volume of f,D holds middle_sum (f,F) = Sum F; definition let A be non empty closed_interval Subset of REAL; let f be Function of A,COMPLEX; let T be DivSequence of A; mode middle_volume_Sequence of f,T -> Function of NAT,(COMPLEX *) means :Def3: :: INTEGR16:def 3 for k being Element of NAT holds it . k is middle_volume of f,T . k; correctness existence ex b1 being Function of NAT,(COMPLEX *) st for k being Element of NAT holds b1 . k is middle_volume of f,T . k; proof defpred S1[ Element of NAT , set ] means \$2 is middle_volume of f,T . \$1; A1: for x being Element of NAT ex y being Element of COMPLEX * st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of COMPLEX * st S1[x,y] set y = the middle_volume of f,T . x; reconsider y = the middle_volume of f,T . x as Element of COMPLEX * by FINSEQ_1:def_11; y is middle_volume of f,T . x ; hence ex y being Element of COMPLEX * st S1[x,y] ; ::_thesis: verum end; ex f being Function of NAT,(COMPLEX *) st for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A1); hence ex b1 being Function of NAT,(COMPLEX *) st for k being Element of NAT holds b1 . k is middle_volume of f,T . k ; ::_thesis: verum end; end; :: deftheorem Def3 defines middle_volume_Sequence INTEGR16:def_3_:_ for A being non empty closed_interval Subset of REAL for f being Function of A,COMPLEX for T being DivSequence of A for b4 being Function of NAT,(COMPLEX *) holds ( b4 is middle_volume_Sequence of f,T iff for k being Element of NAT holds b4 . k is middle_volume of f,T . k ); definition let A be non empty closed_interval Subset of REAL; let f be Function of A,COMPLEX; let T be DivSequence of A; let S be middle_volume_Sequence of f,T; let k be Element of NAT ; :: original: . redefine funcS . k -> middle_volume of f,T . k; coherence S . k is middle_volume of f,T . k by Def3; end; definition let A be non empty closed_interval Subset of REAL; let f be Function of A,COMPLEX; let T be DivSequence of A; let S be middle_volume_Sequence of f,T; func middle_sum (f,S) -> Complex_Sequence means :Def4: :: INTEGR16:def 4 for i being Element of NAT holds it . i = middle_sum (f,(S . i)); existence ex b1 being Complex_Sequence st for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) proof deffunc H1( Element of NAT ) -> Element of COMPLEX = middle_sum (f,(S . \$1)); thus ex IT being Complex_Sequence st for i being Element of NAT holds IT . i = H1(i) from FUNCT_2:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Complex_Sequence st ( for i being Element of NAT holds b1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds b2 . i = middle_sum (f,(S . i)) ) holds b1 = b2 proof let F1, F2 be Complex_Sequence; ::_thesis: ( ( for i being Element of NAT holds F1 . i = middle_sum (f,(S . i)) ) & ( for i being Element of NAT holds F2 . i = middle_sum (f,(S . i)) ) implies F1 = F2 ) assume that A1: for i being Element of NAT holds F1 . i = middle_sum (f,(S . i)) and A2: for i being Element of NAT holds F2 . i = middle_sum (f,(S . i)) ; ::_thesis: F1 = F2 for i being Element of NAT holds F1 . i = F2 . i proof let i be Element of NAT ; ::_thesis: F1 . i = F2 . i F1 . i = middle_sum (f,(S . i)) by A1 .= F2 . i by A2 ; hence F1 . i = F2 . i ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def4 defines middle_sum INTEGR16:def_4_:_ for A being non empty closed_interval Subset of REAL for f being Function of A,COMPLEX for T being DivSequence of A for S being middle_volume_Sequence of f,T for b5 being Complex_Sequence holds ( b5 = middle_sum (f,S) iff for i being Element of NAT holds b5 . i = middle_sum (f,(S . i)) ); begin theorem :: INTEGR16:2 for f being PartFunc of REAL,COMPLEX for A being Subset of REAL holds Re (f | A) = (Re f) | A proof let f be PartFunc of REAL,COMPLEX; ::_thesis: for A being Subset of REAL holds Re (f | A) = (Re f) | A let A be Subset of REAL; ::_thesis: Re (f | A) = (Re f) | A A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((Re_f)_|_A)_holds_ ((Re_f)_|_A)_._c_=_(Re_(f_|_A))_._c let c be set ; ::_thesis: ( c in dom ((Re f) | A) implies ((Re f) | A) . c = (Re (f | A)) . c ) assume A2: c in dom ((Re f) | A) ; ::_thesis: ((Re f) | A) . c = (Re (f | A)) . c then A3: c in (dom (Re f)) /\ A by RELAT_1:61; then A4: c in A by XBOOLE_0:def_4; A5: c in dom (Re f) by A3, XBOOLE_0:def_4; then c in dom f by COMSEQ_3:def_3; then c in (dom f) /\ A by A4, XBOOLE_0:def_4; then A6: c in dom (f | A) by RELAT_1:61; then c in dom (Re (f | A)) by COMSEQ_3:def_3; then (Re (f | A)) . c = Re ((f | A) . c) by COMSEQ_3:def_3 .= Re (f . c) by A6, FUNCT_1:47 .= (Re f) . c by A5, COMSEQ_3:def_3 ; hence ((Re f) | A) . c = (Re (f | A)) . c by A2, FUNCT_1:47; ::_thesis: verum end; dom ((Re f) | A) = (dom (Re f)) /\ A by RELAT_1:61 .= (dom f) /\ A by COMSEQ_3:def_3 .= dom (f | A) by RELAT_1:61 .= dom (Re (f | A)) by COMSEQ_3:def_3 ; hence Re (f | A) = (Re f) | A by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: INTEGR16:3 for f being PartFunc of REAL,COMPLEX for A being Subset of REAL holds Im (f | A) = (Im f) | A proof let f be PartFunc of REAL,COMPLEX; ::_thesis: for A being Subset of REAL holds Im (f | A) = (Im f) | A let A be Subset of REAL; ::_thesis: Im (f | A) = (Im f) | A A1: now__::_thesis:_for_c_being_set_st_c_in_dom_((Im_f)_|_A)_holds_ ((Im_f)_|_A)_._c_=_(Im_(f_|_A))_._c let c be set ; ::_thesis: ( c in dom ((Im f) | A) implies ((Im f) | A) . c = (Im (f | A)) . c ) assume A2: c in dom ((Im f) | A) ; ::_thesis: ((Im f) | A) . c = (Im (f | A)) . c then A3: c in (dom (Im f)) /\ A by RELAT_1:61; then A4: c in A by XBOOLE_0:def_4; A5: c in dom (Im f) by A3, XBOOLE_0:def_4; then c in dom f by COMSEQ_3:def_4; then c in (dom f) /\ A by A4, XBOOLE_0:def_4; then A6: c in dom (f | A) by RELAT_1:61; then c in dom (Im (f | A)) by COMSEQ_3:def_4; then (Im (f | A)) . c = Im ((f | A) . c) by COMSEQ_3:def_4 .= Im (f . c) by A6, FUNCT_1:47 .= (Im f) . c by A5, COMSEQ_3:def_4 ; hence ((Im f) | A) . c = (Im (f | A)) . c by A2, FUNCT_1:47; ::_thesis: verum end; dom ((Im f) | A) = (dom (Im f)) /\ A by RELAT_1:61 .= (dom f) /\ A by COMSEQ_3:def_4 .= dom (f | A) by RELAT_1:61 .= dom (Im (f | A)) by COMSEQ_3:def_4 ; hence Im (f | A) = (Im f) | A by A1, FUNCT_1:2; ::_thesis: verum end; registration let A be non empty closed_interval Subset of REAL; let f be Function of A,COMPLEX; cluster Re f -> quasi_total for PartFunc of A,REAL; correctness coherence for b1 being PartFunc of A,REAL st b1 = Re f holds b1 is quasi_total ; proof dom f = A by FUNCT_2:def_1; then dom (Re f) = A by COMSEQ_3:def_3; hence for b1 being PartFunc of A,REAL st b1 = Re f holds b1 is quasi_total by FUNCT_2:def_1; ::_thesis: verum end; cluster Im f -> quasi_total for PartFunc of A,REAL; correctness coherence for b1 being PartFunc of A,REAL st b1 = Im f holds b1 is quasi_total ; proof dom f = A by FUNCT_2:def_1; then dom (Im f) = A by COMSEQ_3:def_4; hence for b1 being PartFunc of A,REAL st b1 = Im f holds b1 is quasi_total by FUNCT_2:def_1; ::_thesis: verum end; end; theorem Th4: :: INTEGR16:4 for A being non empty closed_interval Subset of REAL for f being Function of A,COMPLEX for D being Division of A for S being middle_volume of f,D holds ( Re S is middle_volume of Re f,D & Im S is middle_volume of Im f,D ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,COMPLEX for D being Division of A for S being middle_volume of f,D holds ( Re S is middle_volume of Re f,D & Im S is middle_volume of Im f,D ) let f be Function of A,COMPLEX; ::_thesis: for D being Division of A for S being middle_volume of f,D holds ( Re S is middle_volume of Re f,D & Im S is middle_volume of Im f,D ) let D be Division of A; ::_thesis: for S being middle_volume of f,D holds ( Re S is middle_volume of Re f,D & Im S is middle_volume of Im f,D ) let S be middle_volume of f,D; ::_thesis: ( Re S is middle_volume of Re f,D & Im S is middle_volume of Im f,D ) A1: dom S = dom (Re S) by COMSEQ_3:def_3; set RS = Re S; len S = len D by Def1; then A2: dom S = Seg (len D) by FINSEQ_1:def_3; then A3: len (Re S) = len D by A1, FINSEQ_1:def_3; for i being Nat st i in dom D holds ex r being Element of REAL st ( r in rng ((Re f) | (divset (D,i))) & (Re S) . i = r * (vol (divset (D,i))) ) proof let i be Nat; ::_thesis: ( i in dom D implies ex r being Element of REAL st ( r in rng ((Re f) | (divset (D,i))) & (Re S) . i = r * (vol (divset (D,i))) ) ) assume A4: i in dom D ; ::_thesis: ex r being Element of REAL st ( r in rng ((Re f) | (divset (D,i))) & (Re S) . i = r * (vol (divset (D,i))) ) consider c being Element of COMPLEX such that A5: ( c in rng (f | (divset (D,i))) & S . i = c * (vol (divset (D,i))) ) by A4, Def1; A6: i in dom (Re S) by A4, A1, A2, FINSEQ_1:def_3; set r = Re c; take Re c ; ::_thesis: ( Re c in rng ((Re f) | (divset (D,i))) & (Re S) . i = (Re c) * (vol (divset (D,i))) ) consider t being set such that A7: t in dom (f | (divset (D,i))) and A8: c = (f | (divset (D,i))) . t by A5, FUNCT_1:def_3; t in (dom f) /\ (divset (D,i)) by A7, RELAT_1:61; then t in dom f by XBOOLE_0:def_4; then A9: t in dom (Re f) by COMSEQ_3:def_3; A10: dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) by RELAT_1:61 .= (dom (Re f)) /\ (divset (D,i)) by COMSEQ_3:def_3 .= dom ((Re f) | (divset (D,i))) by RELAT_1:61 ; Re c = Re (f . t) by A7, A8, FUNCT_1:47 .= (Re f) . t by A9, COMSEQ_3:def_3 .= ((Re f) | (divset (D,i))) . t by A7, A10, FUNCT_1:47 ; hence Re c in rng ((Re f) | (divset (D,i))) by A7, A10, FUNCT_1:def_3; ::_thesis: (Re S) . i = (Re c) * (vol (divset (D,i))) thus (Re S) . i = Re (S . i) by A6, COMSEQ_3:def_3 .= (Re c) * (vol (divset (D,i))) by A5, Th1 ; ::_thesis: verum end; hence Re S is middle_volume of Re f,D by A3, INTEGR15:def_1; ::_thesis: Im S is middle_volume of Im f,D A11: dom S = dom (Im S) by COMSEQ_3:def_4; set IS = Im S; A12: len (Im S) = len D by A2, A11, FINSEQ_1:def_3; for i being Nat st i in dom D holds ex r being Element of REAL st ( r in rng ((Im f) | (divset (D,i))) & (Im S) . i = r * (vol (divset (D,i))) ) proof let i be Nat; ::_thesis: ( i in dom D implies ex r being Element of REAL st ( r in rng ((Im f) | (divset (D,i))) & (Im S) . i = r * (vol (divset (D,i))) ) ) assume A13: i in dom D ; ::_thesis: ex r being Element of REAL st ( r in rng ((Im f) | (divset (D,i))) & (Im S) . i = r * (vol (divset (D,i))) ) consider c being Element of COMPLEX such that A14: ( c in rng (f | (divset (D,i))) & S . i = c * (vol (divset (D,i))) ) by A13, Def1; A15: i in dom (Im S) by A13, A2, A11, FINSEQ_1:def_3; set r = Im c; take Im c ; ::_thesis: ( Im c in rng ((Im f) | (divset (D,i))) & (Im S) . i = (Im c) * (vol (divset (D,i))) ) consider t being set such that A16: t in dom (f | (divset (D,i))) and A17: c = (f | (divset (D,i))) . t by A14, FUNCT_1:def_3; t in (dom f) /\ (divset (D,i)) by A16, RELAT_1:61; then t in dom f by XBOOLE_0:def_4; then A18: t in dom (Im f) by COMSEQ_3:def_4; A19: dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) by RELAT_1:61 .= (dom (Im f)) /\ (divset (D,i)) by COMSEQ_3:def_4 .= dom ((Im f) | (divset (D,i))) by RELAT_1:61 ; Im c = Im (f . t) by A16, A17, FUNCT_1:47 .= (Im f) . t by A18, COMSEQ_3:def_4 .= ((Im f) | (divset (D,i))) . t by A16, A19, FUNCT_1:47 ; hence Im c in rng ((Im f) | (divset (D,i))) by A16, A19, FUNCT_1:def_3; ::_thesis: (Im S) . i = (Im c) * (vol (divset (D,i))) thus (Im S) . i = Im (S . i) by A15, COMSEQ_3:def_4 .= (Im c) * (vol (divset (D,i))) by A14, Th1 ; ::_thesis: verum end; hence Im S is middle_volume of Im f,D by A12, INTEGR15:def_1; ::_thesis: verum end; Lm2: Sum (<*> COMPLEX) = 0 by BINOP_2:1, FINSOP_1:10; Lm3: for F being FinSequence of COMPLEX for x being Element of COMPLEX holds Sum (F ^ <*x*>) = (Sum F) + x proof let F be FinSequence of COMPLEX ; ::_thesis: for x being Element of COMPLEX holds Sum (F ^ <*x*>) = (Sum F) + x let x be Element of COMPLEX ; ::_thesis: Sum (F ^ <*x*>) = (Sum F) + x thus Sum (F ^ <*x*>) = addcomplex . ((addcomplex \$\$ F),x) by FINSOP_1:4 .= (Sum F) + x by BINOP_2:def_3 ; ::_thesis: verum end; theorem Th5: :: INTEGR16:5 for F being FinSequence of COMPLEX for x being Element of COMPLEX holds Re (F ^ <*x*>) = (Re F) ^ <*(Re x)*> proof let F be FinSequence of COMPLEX ; ::_thesis: for x being Element of COMPLEX holds Re (F ^ <*x*>) = (Re F) ^ <*(Re x)*> let x be Element of COMPLEX ; ::_thesis: Re (F ^ <*x*>) = (Re F) ^ <*(Re x)*> set F1 = Re (F ^ <*x*>); set F2 = (Re F) ^ <*(Re x)*>; A1: dom F = dom (Re F) by COMSEQ_3:def_3; A2: Seg (len F) = dom F by FINSEQ_1:def_3; A3: len <*(Re x)*> = 1 by FINSEQ_1:39; A4: dom (Re (F ^ <*x*>)) = dom (F ^ <*x*>) by COMSEQ_3:def_3 .= Seg ((len F) + (len <*x*>)) by FINSEQ_1:def_7 .= Seg ((len (Re F)) + (len <*x*>)) by A1, A2, FINSEQ_1:def_3 .= Seg ((len (Re F)) + (len <*(Re x)*>)) by A3, FINSEQ_1:39 .= dom ((Re F) ^ <*(Re x)*>) by FINSEQ_1:def_7 ; now__::_thesis:_for_k_being_Nat_st_k_in_dom_(Re_(F_^_<*x*>))_holds_ (Re_(F_^_<*x*>))_._k_=_((Re_F)_^_<*(Re_x)*>)_._k let k be Nat; ::_thesis: ( k in dom (Re (F ^ <*x*>)) implies (Re (F ^ <*x*>)) . k = ((Re F) ^ <*(Re x)*>) . k ) assume A5: k in dom (Re (F ^ <*x*>)) ; ::_thesis: (Re (F ^ <*x*>)) . k = ((Re F) ^ <*(Re x)*>) . k then k in dom (F ^ <*x*>) by COMSEQ_3:def_3; then A6: k in Seg (len (F ^ <*x*>)) by FINSEQ_1:def_3; then k in Seg ((len F) + (len <*x*>)) by FINSEQ_1:22; then A7: ( 1 <= k & k <= (len F) + (len <*x*>) ) by FINSEQ_1:1; now__::_thesis:_(Re_(F_^_<*x*>))_._k_=_((Re_F)_^_<*(Re_x)*>)_._k percases ( k = (len F) + 1 or k <> (len F) + 1 ) ; supposeA8: k = (len F) + 1 ; ::_thesis: (Re (F ^ <*x*>)) . k = ((Re F) ^ <*(Re x)*>) . k thus (Re (F ^ <*x*>)) . k = Re ((F ^ <*x*>) . k) by A5, COMSEQ_3:def_3 .= Re x by A8, FINSEQ_1:42 .= ((Re F) ^ <*(Re x)*>) . ((len (Re F)) + 1) by FINSEQ_1:42 .= ((Re F) ^ <*(Re x)*>) . k by A8, A1, A2, FINSEQ_1:def_3 ; ::_thesis: verum end; supposeA9: k <> (len F) + 1 ; ::_thesis: (Re (F ^ <*x*>)) . k = ((Re F) ^ <*(Re x)*>) . k k <= (len F) + 1 by A7, FINSEQ_1:39; then k < (len F) + 1 by A9, XXREAL_0:1; then ( 1 <= k & k <= len F ) by A6, FINSEQ_1:1, NAT_1:13; then k in Seg (len F) by FINSEQ_1:1; then A10: k in dom F by FINSEQ_1:def_3; then A11: k in dom (Re F) by COMSEQ_3:def_3; thus (Re (F ^ <*x*>)) . k = Re ((F ^ <*x*>) . k) by A5, COMSEQ_3:def_3 .= Re (F . k) by A10, FINSEQ_1:def_7 .= (Re F) . k by A11, COMSEQ_3:def_3 .= ((Re F) ^ <*(Re x)*>) . k by A11, FINSEQ_1:def_7 ; ::_thesis: verum end; end; end; hence (Re (F ^ <*x*>)) . k = ((Re F) ^ <*(Re x)*>) . k ; ::_thesis: verum end; hence Re (F ^ <*x*>) = (Re F) ^ <*(Re x)*> by A4, FINSEQ_1:13; ::_thesis: verum end; theorem Th6: :: INTEGR16:6 for F being FinSequence of COMPLEX for x being Element of COMPLEX holds Im (F ^ <*x*>) = (Im F) ^ <*(Im x)*> proof let F be FinSequence of COMPLEX ; ::_thesis: for x being Element of COMPLEX holds Im (F ^ <*x*>) = (Im F) ^ <*(Im x)*> let x be Element of COMPLEX ; ::_thesis: Im (F ^ <*x*>) = (Im F) ^ <*(Im x)*> set F1 = Im (F ^ <*x*>); set F2 = (Im F) ^ <*(Im x)*>; A1: dom F = dom (Im F) by COMSEQ_3:def_4; A2: Seg (len F) = dom F by FINSEQ_1:def_3; A3: len <*(Im x)*> = 1 by FINSEQ_1:39; A4: dom (Im (F ^ <*x*>)) = dom (F ^ <*x*>) by COMSEQ_3:def_4 .= Seg ((len F) + (len <*x*>)) by FINSEQ_1:def_7 .= Seg ((len (Im F)) + (len <*x*>)) by A1, A2, FINSEQ_1:def_3 .= Seg ((len (Im F)) + (len <*(Im x)*>)) by A3, FINSEQ_1:39 .= dom ((Im F) ^ <*(Im x)*>) by FINSEQ_1:def_7 ; now__::_thesis:_for_k_being_Nat_st_k_in_dom_(Im_(F_^_<*x*>))_holds_ (Im_(F_^_<*x*>))_._k_=_((Im_F)_^_<*(Im_x)*>)_._k let k be Nat; ::_thesis: ( k in dom (Im (F ^ <*x*>)) implies (Im (F ^ <*x*>)) . k = ((Im F) ^ <*(Im x)*>) . k ) assume A5: k in dom (Im (F ^ <*x*>)) ; ::_thesis: (Im (F ^ <*x*>)) . k = ((Im F) ^ <*(Im x)*>) . k then k in dom (F ^ <*x*>) by COMSEQ_3:def_4; then A6: k in Seg (len (F ^ <*x*>)) by FINSEQ_1:def_3; then k in Seg ((len F) + (len <*x*>)) by FINSEQ_1:22; then A7: ( 1 <= k & k <= (len F) + (len <*x*>) ) by FINSEQ_1:1; now__::_thesis:_(Im_(F_^_<*x*>))_._k_=_((Im_F)_^_<*(Im_x)*>)_._k percases ( k = (len F) + 1 or k <> (len F) + 1 ) ; supposeA8: k = (len F) + 1 ; ::_thesis: (Im (F ^ <*x*>)) . k = ((Im F) ^ <*(Im x)*>) . k thus (Im (F ^ <*x*>)) . k = Im ((F ^ <*x*>) . k) by A5, COMSEQ_3:def_4 .= Im x by A8, FINSEQ_1:42 .= ((Im F) ^ <*(Im x)*>) . ((len (Im F)) + 1) by FINSEQ_1:42 .= ((Im F) ^ <*(Im x)*>) . k by A8, A1, A2, FINSEQ_1:def_3 ; ::_thesis: verum end; supposeA9: k <> (len F) + 1 ; ::_thesis: (Im (F ^ <*x*>)) . k = ((Im F) ^ <*(Im x)*>) . k k <= (len F) + 1 by A7, FINSEQ_1:39; then k < (len F) + 1 by A9, XXREAL_0:1; then ( 1 <= k & k <= len F ) by A6, FINSEQ_1:1, NAT_1:13; then k in Seg (len F) by FINSEQ_1:1; then A10: k in dom F by FINSEQ_1:def_3; then A11: k in dom (Im F) by COMSEQ_3:def_4; thus (Im (F ^ <*x*>)) . k = Im ((F ^ <*x*>) . k) by A5, COMSEQ_3:def_4 .= Im (F . k) by A10, FINSEQ_1:def_7 .= (Im F) . k by A11, COMSEQ_3:def_4 .= ((Im F) ^ <*(Im x)*>) . k by A11, FINSEQ_1:def_7 ; ::_thesis: verum end; end; end; hence (Im (F ^ <*x*>)) . k = ((Im F) ^ <*(Im x)*>) . k ; ::_thesis: verum end; hence Im (F ^ <*x*>) = (Im F) ^ <*(Im x)*> by A4, FINSEQ_1:13; ::_thesis: verum end; theorem Th7: :: INTEGR16:7 for F being FinSequence of COMPLEX for Fr being FinSequence of REAL st Fr = Re F holds Sum Fr = Re (Sum F) proof defpred S1[ Nat] means for F being FinSequence of COMPLEX for Fr being FinSequence of REAL st len F = \$1 & Fr = Re F holds Sum Fr = Re (Sum F); A1: S1[ 0 ] proof let F be FinSequence of COMPLEX ; ::_thesis: for Fr being FinSequence of REAL st len F = 0 & Fr = Re F holds Sum Fr = Re (Sum F) let Fr be FinSequence of REAL ; ::_thesis: ( len F = 0 & Fr = Re F implies Sum Fr = Re (Sum F) ) assume A2: ( len F = 0 & Fr = Re F ) ; ::_thesis: Sum Fr = Re (Sum F) then dom Fr = dom F by COMSEQ_3:def_3 .= Seg (len F) by FINSEQ_1:def_3 ; then A3: len Fr = 0 by A2, FINSEQ_1:def_3; thus Re (Sum F) = Re 0 by A2, Lm2, FINSEQ_1:20 .= Sum Fr by A3, COMPLEX1:4, FINSEQ_1:20, RVSUM_1:72 ; ::_thesis: verum end; A4: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_F_being_FinSequence_of_COMPLEX_ for_Fr_being_FinSequence_of_REAL_st_len_F_=_k_+_1_&_Fr_=_Re_F_holds_ Re_(Sum_F)_=_Sum_Fr let F be FinSequence of COMPLEX ; ::_thesis: for Fr being FinSequence of REAL st len F = k + 1 & Fr = Re F holds Re (Sum F) = Sum Fr let Fr be FinSequence of REAL ; ::_thesis: ( len F = k + 1 & Fr = Re F implies Re (Sum F) = Sum Fr ) assume A6: ( len F = k + 1 & Fr = Re F ) ; ::_thesis: Re (Sum F) = Sum Fr reconsider F1 = F | k as FinSequence of COMPLEX ; A7: len F1 = k by A6, FINSEQ_1:59, NAT_1:11; reconsider F1r = Re F1 as FinSequence of REAL ; reconsider x = F . (k + 1) as Element of COMPLEX by XCMPLX_0:def_2; A8: F = F1 ^ <*x*> by A6, FINSEQ_3:55; hence Re (Sum F) = Re ((Sum F1) + x) by Lm3 .= (Re (Sum F1)) + (Re x) by COMPLEX1:8 .= (Sum F1r) + (Re x) by A5, A7 .= Sum (F1r ^ <*(Re x)*>) by RVSUM_1:74 .= Sum Fr by A6, A8, Th5 ; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A9: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A1, A4); let F be FinSequence of COMPLEX ; ::_thesis: for Fr being FinSequence of REAL st Fr = Re F holds Sum Fr = Re (Sum F) let Fr be FinSequence of REAL ; ::_thesis: ( Fr = Re F implies Sum Fr = Re (Sum F) ) assume A10: Fr = Re F ; ::_thesis: Sum Fr = Re (Sum F) len F is Element of NAT ; hence Sum Fr = Re (Sum F) by A9, A10; ::_thesis: verum end; theorem Th8: :: INTEGR16:8 for F being FinSequence of COMPLEX for Fi being FinSequence of REAL st Fi = Im F holds Sum Fi = Im (Sum F) proof defpred S1[ Nat] means for F being FinSequence of COMPLEX for Fi being FinSequence of REAL st len F = \$1 & Fi = Im F holds Sum Fi = Im (Sum F); A1: S1[ 0 ] proof let F be FinSequence of COMPLEX ; ::_thesis: for Fi being FinSequence of REAL st len F = 0 & Fi = Im F holds Sum Fi = Im (Sum F) let Fi be FinSequence of REAL ; ::_thesis: ( len F = 0 & Fi = Im F implies Sum Fi = Im (Sum F) ) assume A2: ( len F = 0 & Fi = Im F ) ; ::_thesis: Sum Fi = Im (Sum F) then dom Fi = dom F by COMSEQ_3:def_4 .= Seg (len F) by FINSEQ_1:def_3 ; then A3: len Fi = 0 by A2, FINSEQ_1:def_3; thus Im (Sum F) = Im 0 by A2, Lm2, FINSEQ_1:20 .= Sum Fi by A3, COMPLEX1:4, FINSEQ_1:20, RVSUM_1:72 ; ::_thesis: verum end; A4: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_F_being_FinSequence_of_COMPLEX_ for_Fi_being_FinSequence_of_REAL_st_len_F_=_k_+_1_&_Fi_=_Im_F_holds_ Im_(Sum_F)_=_Sum_Fi let F be FinSequence of COMPLEX ; ::_thesis: for Fi being FinSequence of REAL st len F = k + 1 & Fi = Im F holds Im (Sum F) = Sum Fi let Fi be FinSequence of REAL ; ::_thesis: ( len F = k + 1 & Fi = Im F implies Im (Sum F) = Sum Fi ) assume A6: ( len F = k + 1 & Fi = Im F ) ; ::_thesis: Im (Sum F) = Sum Fi reconsider F1 = F | k as FinSequence of COMPLEX ; A7: len F1 = k by A6, FINSEQ_1:59, NAT_1:11; reconsider F1i = Im F1 as FinSequence of REAL ; reconsider x = F . (k + 1) as Element of COMPLEX by XCMPLX_0:def_2; A8: F = F1 ^ <*x*> by A6, FINSEQ_3:55; hence Im (Sum F) = Im ((Sum F1) + x) by Lm3 .= (Im (Sum F1)) + (Im x) by COMPLEX1:8 .= (Sum F1i) + (Im x) by A5, A7 .= Sum (F1i ^ <*(Im x)*>) by RVSUM_1:74 .= Sum Fi by A6, A8, Th6 ; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A9: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A1, A4); let F be FinSequence of COMPLEX ; ::_thesis: for Fi being FinSequence of REAL st Fi = Im F holds Sum Fi = Im (Sum F) let Fi be FinSequence of REAL ; ::_thesis: ( Fi = Im F implies Sum Fi = Im (Sum F) ) assume A10: Fi = Im F ; ::_thesis: Sum Fi = Im (Sum F) len F is Element of NAT ; hence Sum Fi = Im (Sum F) by A9, A10; ::_thesis: verum end; theorem :: INTEGR16:9 for A being non empty closed_interval Subset of REAL for f being Function of A,COMPLEX for D being Division of A for F being middle_volume of f,D for Fr being middle_volume of Re f,D st Fr = Re F holds Re (middle_sum (f,F)) = middle_sum ((Re f),Fr) by Th7; theorem :: INTEGR16:10 for A being non empty closed_interval Subset of REAL for f being Function of A,COMPLEX for D being Division of A for F being middle_volume of f,D for Fi being middle_volume of Im f,D st Fi = Im F holds Im (middle_sum (f,F)) = middle_sum ((Im f),Fi) by Th8; definition let A be non empty closed_interval Subset of REAL; let f be Function of A,COMPLEX; attrf is integrable means :Def5: :: INTEGR16:def 5 ( Re f is integrable & Im f is integrable ); end; :: deftheorem Def5 defines integrable INTEGR16:def_5_:_ for A being non empty closed_interval Subset of REAL for f being Function of A,COMPLEX holds ( f is integrable iff ( Re f is integrable & Im f is integrable ) ); theorem Th11: :: INTEGR16:11 for f being PartFunc of REAL,COMPLEX holds ( f is bounded iff ( Re f is bounded & Im f is bounded ) ) proof let f be PartFunc of REAL,COMPLEX; ::_thesis: ( f is bounded iff ( Re f is bounded & Im f is bounded ) ) thus ( f is bounded implies ( Re f is bounded & Im f is bounded ) ) ::_thesis: ( Re f is bounded & Im f is bounded implies f is bounded ) proof assume f is bounded ; ::_thesis: ( Re f is bounded & Im f is bounded ) then consider r being real number such that A1: for y being set st y in dom f holds abs (f . y) < r by COMSEQ_2:def_3; now__::_thesis:_for_y_being_set_st_y_in_dom_(Re_f)_holds_ abs_((Re_f)_._y)_<_r let y be set ; ::_thesis: ( y in dom (Re f) implies abs ((Re f) . y) < r ) assume A2: y in dom (Re f) ; ::_thesis: abs ((Re f) . y) < r then A3: y in dom f by COMSEQ_3:def_3; abs (Re (f . y)) <= abs (f . y) by COMPLEX1:79; then abs (Re (f . y)) < r by A1, A3, XXREAL_0:2; hence abs ((Re f) . y) < r by A2, COMSEQ_3:def_3; ::_thesis: verum end; hence Re f is bounded by COMSEQ_2:def_3; ::_thesis: Im f is bounded now__::_thesis:_for_y_being_set_st_y_in_dom_(Im_f)_holds_ abs_((Im_f)_._y)_<_r let y be set ; ::_thesis: ( y in dom (Im f) implies abs ((Im f) . y) < r ) assume A4: y in dom (Im f) ; ::_thesis: abs ((Im f) . y) < r then A5: y in dom f by COMSEQ_3:def_4; abs (Im (f . y)) <= abs (f . y) by COMPLEX1:79; then abs (Im (f . y)) < r by A1, A5, XXREAL_0:2; hence abs ((Im f) . y) < r by A4, COMSEQ_3:def_4; ::_thesis: verum end; hence Im f is bounded by COMSEQ_2:def_3; ::_thesis: verum end; thus ( Re f is bounded & Im f is bounded implies f is bounded ) ::_thesis: verum proof assume A6: ( Re f is bounded & Im f is bounded ) ; ::_thesis: f is bounded then consider r1 being real number such that A7: for y being set st y in dom (Re f) holds abs ((Re f) . y) < r1 by COMSEQ_2:def_3; consider r2 being real number such that A8: for y being set st y in dom (Im f) holds abs ((Im f) . y) < r2 by A6, COMSEQ_2:def_3; now__::_thesis:_for_y_being_set_st_y_in_dom_f_holds_ abs_(f_._y)_<_r1_+_r2 let y be set ; ::_thesis: ( y in dom f implies abs (f . y) < r1 + r2 ) assume A9: y in dom f ; ::_thesis: abs (f . y) < r1 + r2 then A10: y in dom (Re f) by COMSEQ_3:def_3; then abs ((Re f) . y) < r1 by A7; then A11: abs (Re (f . y)) < r1 by A10, COMSEQ_3:def_3; A12: y in dom (Im f) by A9, COMSEQ_3:def_4; then abs ((Im f) . y) < r2 by A8; then A13: abs (Im (f . y)) < r2 by A12, COMSEQ_3:def_4; A14: abs (f . y) <= (abs (Re (f . y))) + (abs (Im (f . y))) by COMPLEX1:78; (abs (Re (f . y))) + (abs (Im (f . y))) < r1 + r2 by A11, A13, XREAL_1:8; hence abs (f . y) < r1 + r2 by A14, XXREAL_0:2; ::_thesis: verum end; hence f is bounded by COMSEQ_2:def_3; ::_thesis: verum end; end; theorem :: INTEGR16:12 for A being non empty Subset of REAL for f being PartFunc of REAL,COMPLEX for g being Function of A,COMPLEX st f = g holds ( Re f = Re g & Im f = Im g ) ; theorem Th13: :: INTEGR16:13 for A being non empty closed_interval Subset of REAL for f being Function of A,COMPLEX holds ( f is bounded iff ( Re f is bounded & Im f is bounded ) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,COMPLEX holds ( f is bounded iff ( Re f is bounded & Im f is bounded ) ) let f be Function of A,COMPLEX; ::_thesis: ( f is bounded iff ( Re f is bounded & Im f is bounded ) ) dom f = A by FUNCT_2:def_1; then reconsider f0 = f as PartFunc of REAL,COMPLEX by RELSET_1:5; ( f0 is bounded iff ( Re f0 is bounded & Im f0 is bounded ) ) by Th11; hence ( f is bounded iff ( Re f is bounded & Im f is bounded ) ) ; ::_thesis: verum end; definition let A be non empty closed_interval Subset of REAL; let f be Function of A,COMPLEX; func integral f -> Element of COMPLEX equals :: INTEGR16:def 6 (integral (Re f)) + ((integral (Im f)) * ); correctness coherence (integral (Re f)) + ((integral (Im f)) * ) is Element of COMPLEX ; ; end; :: deftheorem defines integral INTEGR16:def_6_:_ for A being non empty closed_interval Subset of REAL for f being Function of A,COMPLEX holds integral f = (integral (Re f)) + ((integral (Im f)) * ); theorem Th14: :: INTEGR16:14 for A being non empty closed_interval Subset of REAL for f being Function of A,COMPLEX for T being DivSequence of A for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,COMPLEX for T being DivSequence of A for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) let f be Function of A,COMPLEX; ::_thesis: for T being DivSequence of A for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) let T be DivSequence of A; ::_thesis: for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) let S be middle_volume_Sequence of f,T; ::_thesis: ( f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 implies ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) ) assume that A1: ( f is bounded & f is integrable ) and A2: ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = integral f ) set seq = middle_sum (f,S); set xs = integral f; A3: ( Re f is bounded & Re f is integrable ) by A1, Def5, Th13; A4: ( Im f is bounded & Im f is integrable ) by A1, Def5, Th13; reconsider xseq = middle_sum (f,S) as Function of NAT,COMPLEX ; ex rseqi being Real_Sequence st for k being Element of NAT holds ( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi ) proof reconsider pjinf = Re f as Function of A,REAL ; defpred S1[ Element of NAT , set ] means \$2 = Re (S . \$1); A5: for x being Element of NAT ex y being Element of REAL * st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of REAL * st S1[x,y] Re (S . x) is Element of REAL * by FINSEQ_1:def_11; hence ex y being Element of REAL * st S1[x,y] ; ::_thesis: verum end; consider F being Function of NAT,(REAL *) such that A6: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch_3(A5); A7: for x being Element of NAT holds dom (Re (S . x)) = Seg (len (S . x)) proof let x be Element of NAT ; ::_thesis: dom (Re (S . x)) = Seg (len (S . x)) thus dom (Re (S . x)) = dom (S . x) by COMSEQ_3:def_3 .= Seg (len (S . x)) by FINSEQ_1:def_3 ; ::_thesis: verum end; for k being Element of NAT holds F . k is middle_volume of pjinf,T . k proof let k be Element of NAT ; ::_thesis: F . k is middle_volume of pjinf,T . k set Tk = T . k; reconsider Fk = F . k as FinSequence of REAL by FINSEQ_1:def_11; A8: F . k = Re (S . k) by A6; then A9: dom Fk = Seg (len (S . k)) by A7 .= Seg (len (T . k)) by Def1 ; then A10: dom Fk = dom (T . k) by FINSEQ_1:def_3; A11: now__::_thesis:_for_j_being_Nat_st_j_in_dom_(T_._k)_holds_ ex_v_being_Element_of_REAL_st_ (_v_in_rng_(pjinf_|_(divset_((T_._k),j)))_&_Fk_._j_=_v_*_(vol_(divset_((T_._k),j)))_) let j be Nat; ::_thesis: ( j in dom (T . k) implies ex v being Element of REAL st ( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) ) ) assume A12: j in dom (T . k) ; ::_thesis: ex v being Element of REAL st ( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) ) then consider r being Element of COMPLEX such that A13: r in rng (f | (divset ((T . k),j))) and A14: (S . k) . j = r * (vol (divset ((T . k),j))) by Def1; reconsider v = Re r as Element of REAL ; take v = v; ::_thesis: ( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) ) consider t being set such that A15: t in dom (f | (divset ((T . k),j))) and A16: r = (f | (divset ((T . k),j))) . t by A13, FUNCT_1:def_3; t in (dom f) /\ (divset ((T . k),j)) by A15, RELAT_1:61; then t in dom f by XBOOLE_0:def_4; then A17: t in dom (Re f) by COMSEQ_3:def_3; A18: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61 .= (dom pjinf) /\ (divset ((T . k),j)) by COMSEQ_3:def_3 .= dom (pjinf | (divset ((T . k),j))) by RELAT_1:61 ; Re r = Re (f . t) by A15, A16, FUNCT_1:47 .= (Re f) . t by A17, COMSEQ_3:def_3 .= (pjinf | (divset ((T . k),j))) . t by A15, A18, FUNCT_1:47 ; hence v in rng (pjinf | (divset ((T . k),j))) by A15, A18, FUNCT_1:3; ::_thesis: Fk . j = v * (vol (divset ((T . k),j))) thus Fk . j = Re ((S . k) . j) by A8, A10, A12, COMSEQ_3:def_3 .= v * (vol (divset ((T . k),j))) by A14, Th1 ; ::_thesis: verum end; len Fk = len (T . k) by A9, FINSEQ_1:def_3; hence F . k is middle_volume of pjinf,T . k by A11, INTEGR15:def_1; ::_thesis: verum end; then reconsider pjis = F as middle_volume_Sequence of pjinf,T by INTEGR15:def_3; reconsider rseqi = middle_sum (pjinf,pjis) as Real_Sequence ; A19: for k being Element of NAT holds rseqi . k = Re (xseq . k) proof let k be Element of NAT ; ::_thesis: rseqi . k = Re (xseq . k) A20: Re (S . k) is middle_volume of Re f,T . k by Th4; thus rseqi . k = middle_sum (pjinf,(pjis . k)) by INTEGR15:def_4 .= Re (middle_sum (f,(S . k))) by A6, A20, Th7 .= Re (xseq . k) by Def4 ; ::_thesis: verum end; take rseqi ; ::_thesis: for k being Element of NAT holds ( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi ) lim (middle_sum (pjinf,pjis)) = integral pjinf by A2, A3, INTEGR15:9; hence for k being Element of NAT holds ( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi ) by A2, A3, A19, COMPLEX1:12, INTEGR15:9; ::_thesis: verum end; then consider rseqi being Real_Sequence such that A21: for k being Element of NAT holds ( rseqi . k = Re (xseq . k) & rseqi is convergent & Re (integral f) = lim rseqi ) ; ex iseqi being Real_Sequence st for k being Element of NAT holds ( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi ) proof reconsider pjinf = Im f as Function of A,REAL ; defpred S1[ Element of NAT , set ] means \$2 = Im (S . \$1); A22: for x being Element of NAT ex y being Element of REAL * st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of REAL * st S1[x,y] Im (S . x) is Element of REAL * by FINSEQ_1:def_11; hence ex y being Element of REAL * st S1[x,y] ; ::_thesis: verum end; consider F being Function of NAT,(REAL *) such that A23: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch_3(A22); A24: for x being Element of NAT holds dom (Im (S . x)) = Seg (len (S . x)) proof let x be Element of NAT ; ::_thesis: dom (Im (S . x)) = Seg (len (S . x)) dom (Im (S . x)) = dom (S . x) by COMSEQ_3:def_4 .= Seg (len (S . x)) by FINSEQ_1:def_3 ; hence dom (Im (S . x)) = Seg (len (S . x)) ; ::_thesis: verum end; for k being Element of NAT holds F . k is middle_volume of pjinf,T . k proof let k be Element of NAT ; ::_thesis: F . k is middle_volume of pjinf,T . k reconsider Tk = T . k as FinSequence ; reconsider Fk = F . k as FinSequence of REAL by FINSEQ_1:def_11; A25: F . k = Im (S . k) by A23; then A26: dom Fk = Seg (len (S . k)) by A24 .= Seg (len Tk) by Def1 ; then A27: dom Fk = dom Tk by FINSEQ_1:def_3; A28: now__::_thesis:_for_j_being_Nat_st_j_in_dom_Tk_holds_ ex_v_being_Element_of_REAL_st_ (_v_in_rng_(pjinf_|_(divset_((T_._k),j)))_&_Fk_._j_=_v_*_(vol_(divset_((T_._k),j)))_) let j be Nat; ::_thesis: ( j in dom Tk implies ex v being Element of REAL st ( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) ) ) assume A29: j in dom Tk ; ::_thesis: ex v being Element of REAL st ( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) ) then consider r being Element of COMPLEX such that A30: r in rng (f | (divset ((T . k),j))) and A31: (S . k) . j = r * (vol (divset ((T . k),j))) by Def1; reconsider v = Im r as Element of REAL ; take v = v; ::_thesis: ( v in rng (pjinf | (divset ((T . k),j))) & Fk . j = v * (vol (divset ((T . k),j))) ) consider t being set such that A32: t in dom (f | (divset ((T . k),j))) and A33: r = (f | (divset ((T . k),j))) . t by A30, FUNCT_1:def_3; t in (dom f) /\ (divset ((T . k),j)) by A32, RELAT_1:61; then t in dom f by XBOOLE_0:def_4; then A34: t in dom (Im f) by COMSEQ_3:def_4; A35: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61 .= (dom pjinf) /\ (divset ((T . k),j)) by COMSEQ_3:def_4 .= dom (pjinf | (divset ((T . k),j))) by RELAT_1:61 ; Im r = Im (f . t) by A32, A33, FUNCT_1:47 .= (Im f) . t by A34, COMSEQ_3:def_4 .= (pjinf | (divset ((T . k),j))) . t by A32, A35, FUNCT_1:47 ; hence v in rng (pjinf | (divset ((T . k),j))) by A32, A35, FUNCT_1:3; ::_thesis: Fk . j = v * (vol (divset ((T . k),j))) thus Fk . j = Im ((S . k) . j) by A25, A27, A29, COMSEQ_3:def_4 .= v * (vol (divset ((T . k),j))) by A31, Th1 ; ::_thesis: verum end; len Fk = len Tk by A26, FINSEQ_1:def_3; hence F . k is middle_volume of pjinf,T . k by A28, INTEGR15:def_1; ::_thesis: verum end; then reconsider pjis = F as middle_volume_Sequence of pjinf,T by INTEGR15:def_3; reconsider iseqi = middle_sum (pjinf,pjis) as Real_Sequence ; A36: for k being Element of NAT holds iseqi . k = Im (xseq . k) proof let k be Element of NAT ; ::_thesis: iseqi . k = Im (xseq . k) A37: Im (S . k) is middle_volume of Im f,T . k by Th4; thus iseqi . k = middle_sum (pjinf,(pjis . k)) by INTEGR15:def_4 .= Im (middle_sum (f,(S . k))) by A23, A37, Th8 .= Im (xseq . k) by Def4 ; ::_thesis: verum end; take iseqi ; ::_thesis: for k being Element of NAT holds ( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi ) lim (middle_sum (pjinf,pjis)) = integral pjinf by A2, A4, INTEGR15:9; hence for k being Element of NAT holds ( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi ) by A2, A4, A36, COMPLEX1:12, INTEGR15:9; ::_thesis: verum end; then consider iseqi being Real_Sequence such that A38: for k being Element of NAT holds ( iseqi . k = Im (xseq . k) & iseqi is convergent & Im (integral f) = lim iseqi ) ; thus middle_sum (f,S) is convergent by A21, A38, COMSEQ_3:38; ::_thesis: lim (middle_sum (f,S)) = integral f thus lim (middle_sum (f,S)) = (lim rseqi) + ((lim iseqi) * ) by A21, A38, COMSEQ_3:39 .= integral f by A21, A38, COMPLEX1:13 ; ::_thesis: verum end; theorem :: INTEGR16:15 for A being non empty closed_interval Subset of REAL for f being Function of A,COMPLEX st f is bounded holds ( f is integrable iff ex I being Element of COMPLEX st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,COMPLEX st f is bounded holds ( f is integrable iff ex I being Element of COMPLEX st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) let f be Function of A,COMPLEX; ::_thesis: ( f is bounded implies ( f is integrable iff ex I being Element of COMPLEX st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) ) assume A1: f is bounded ; ::_thesis: ( f is integrable iff ex I being Element of COMPLEX st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ) hereby ::_thesis: ( ex I being Element of COMPLEX st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable ) reconsider I = integral f as Element of COMPLEX ; assume A2: f is integrable ; ::_thesis: ex I being Element of COMPLEX st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) take I = I; ::_thesis: for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) thus for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A1, A2, Th14; ::_thesis: verum end; now__::_thesis:_(_ex_I_being_Element_of_COMPLEX_st_ for_T_being_DivSequence_of_A for_S_being_middle_volume_Sequence_of_f,T_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_ (_middle_sum_(f,S)_is_convergent_&_lim_(middle_sum_(f,S))_=_I_)_implies_f_is_integrable_) assume ex I being Element of COMPLEX st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ; ::_thesis: f is integrable then consider I being Element of COMPLEX such that A3: for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) ; reconsider Ii = Re I as Element of REAL ; reconsider Ic = Im I as Element of REAL ; A4: now__::_thesis:_for_T_being_DivSequence_of_A for_Si_being_middle_volume_Sequence_of_Re_f,T_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_ (_middle_sum_((Re_f),Si)_is_convergent_&_lim_(middle_sum_((Re_f),Si))_=_Ii_) set x = I; let T be DivSequence of A; ::_thesis: for Si being middle_volume_Sequence of Re f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii ) let Si be middle_volume_Sequence of Re f,T; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii ) ) defpred S1[ Element of NAT , set ] means ex H, z being FinSequence st ( H = T . \$1 & z = \$2 & len z = len H & ( for j being Element of NAT st j in dom H holds ex rji being Element of COMPLEX ex tji being Element of REAL st ( tji in dom (f | (divset ((T . \$1),j))) & (Si . \$1) . j = (vol (divset ((T . \$1),j))) * (((Re f) | (divset ((T . \$1),j))) . tji) & rji = (f | (divset ((T . \$1),j))) . tji & z . j = (vol (divset ((T . \$1),j))) * rji ) ) ); reconsider xs = I as Element of COMPLEX ; A5: for k being Element of NAT ex y being Element of COMPLEX * st S1[k,y] proof let k be Element of NAT ; ::_thesis: ex y being Element of COMPLEX * st S1[k,y] reconsider Tk = T . k as FinSequence ; defpred S2[ Nat, set ] means ex j being Element of NAT st ( \$1 = j & ex rji being Element of COMPLEX ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & \$2 = (vol (divset ((T . k),j))) * rji ) ); A6: for j being Nat st j in Seg (len Tk) holds ex x being Element of COMPLEX st S2[j,x] proof let j0 be Nat; ::_thesis: ( j0 in Seg (len Tk) implies ex x being Element of COMPLEX st S2[j0,x] ) assume A7: j0 in Seg (len Tk) ; ::_thesis: ex x being Element of COMPLEX st S2[j0,x] then reconsider j = j0 as Element of NAT ; j in dom Tk by A7, FINSEQ_1:def_3; then consider r being Element of REAL such that A8: r in rng ((Re f) | (divset ((T . k),j))) and A9: (Si . k) . j = r * (vol (divset ((T . k),j))) by INTEGR15:def_1; consider tji being set such that A10: tji in dom ((Re f) | (divset ((T . k),j))) and A11: r = ((Re f) | (divset ((T . k),j))) . tji by A8, FUNCT_1:def_3; tji in (dom (Re f)) /\ (divset ((T . k),j)) by A10, RELAT_1:61; then reconsider tji = tji as Element of REAL ; A12: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61 .= (dom (Re f)) /\ (divset ((T . k),j)) by COMSEQ_3:def_3 .= dom ((Re f) | (divset ((T . k),j))) by RELAT_1:61 ; then (f | (divset ((T . k),j))) . tji in rng (f | (divset ((T . k),j))) by A10, FUNCT_1:3; then reconsider rji = (f | (divset ((T . k),j))) . tji as Element of COMPLEX ; reconsider x = (vol (divset ((T . k),j))) * rji as Element of COMPLEX ; take x ; ::_thesis: S2[j0,x] thus S2[j0,x] by A9, A10, A11, A12; ::_thesis: verum end; consider p being FinSequence of COMPLEX such that A13: ( dom p = Seg (len Tk) & ( for j being Nat st j in Seg (len Tk) holds S2[j,p . j] ) ) from FINSEQ_1:sch_5(A6); reconsider x = p as Element of COMPLEX * by FINSEQ_1:def_11; take x ; ::_thesis: S1[k,x] A14: now__::_thesis:_for_jj0_being_Element_of_NAT_st_jj0_in_dom_Tk_holds_ ex_rji_being_Element_of_COMPLEX_ex_tji_being_Element_of_REAL_st_ (_tji_in_dom_(f_|_(divset_((T_._k),jj0)))_&_(Si_._k)_._jj0_=_(vol_(divset_((T_._k),jj0)))_*_(((Re_f)_|_(divset_((T_._k),jj0)))_._tji)_&_rji_=_(f_|_(divset_((T_._k),jj0)))_._tji_&_p_._jj0_=_(vol_(divset_((T_._k),jj0)))_*_rji_) let jj0 be Element of NAT ; ::_thesis: ( jj0 in dom Tk implies ex rji being Element of COMPLEX ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Re f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji ) ) reconsider j0 = jj0 as Nat ; A15: dom Tk = Seg (len Tk) by FINSEQ_1:def_3; assume jj0 in dom Tk ; ::_thesis: ex rji being Element of COMPLEX ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Re f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji ) then S2[j0,p . j0] by A13, A15; hence ex rji being Element of COMPLEX ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Re f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji ) ; ::_thesis: verum end; len p = len Tk by A13, FINSEQ_1:def_3; hence S1[k,x] by A14; ::_thesis: verum end; consider S being Function of NAT,(COMPLEX *) such that A16: for x being Element of NAT holds S1[x,S . x] from FUNCT_2:sch_3(A5); for k being Element of NAT holds S . k is middle_volume of f,T . k proof let k be Element of NAT ; ::_thesis: S . k is middle_volume of f,T . k consider H, z being FinSequence such that A17: ( H = T . k & z = S . k & len H = len z ) and A18: for j being Element of NAT st j in dom H holds ex rji being Element of COMPLEX ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A16; A19: now__::_thesis:_for_x_being_Nat_st_x_in_dom_H_holds_ ex_rji_being_Element_of_COMPLEX_st_ (_rji_in_rng_(f_|_(divset_((T_._k),x)))_&_z_._x_=_rji_*_(vol_(divset_((T_._k),x)))_) let x be Nat; ::_thesis: ( x in dom H implies ex rji being Element of COMPLEX st ( rji in rng (f | (divset ((T . k),x))) & z . x = rji * (vol (divset ((T . k),x))) ) ) assume A20: x in dom H ; ::_thesis: ex rji being Element of COMPLEX st ( rji in rng (f | (divset ((T . k),x))) & z . x = rji * (vol (divset ((T . k),x))) ) then reconsider j = x as Element of NAT ; consider rji being Element of COMPLEX , tji being Element of REAL such that A21: tji in dom (f | (divset ((T . k),j))) and (Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) and A22: rji = (f | (divset ((T . k),j))) . tji and A23: z . j = (vol (divset ((T . k),j))) * rji by A18, A20; take rji = rji; ::_thesis: ( rji in rng (f | (divset ((T . k),x))) & z . x = rji * (vol (divset ((T . k),x))) ) thus rji in rng (f | (divset ((T . k),x))) by A21, A22, FUNCT_1:3; ::_thesis: z . x = rji * (vol (divset ((T . k),x))) thus z . x = rji * (vol (divset ((T . k),x))) by A23; ::_thesis: verum end; S . k is FinSequence of COMPLEX by FINSEQ_1:def_11; hence S . k is middle_volume of f,T . k by A17, A19, Def1; ::_thesis: verum end; then reconsider S = S as middle_volume_Sequence of f,T by Def3; set seq = middle_sum (f,S); reconsider xseq = middle_sum (f,S) as Function of NAT,COMPLEX ; assume ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii ) then A24: ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A3; reconsider rseqi = Re (middle_sum (f,S)) as Real_Sequence ; A25: for k being Element of NAT holds ( rseqi . k = Re (xseq . k) & rseqi is convergent & Re xs = lim rseqi ) by A24, COMSEQ_3:41, COMSEQ_3:def_5; for k being Element of NAT holds rseqi . k = (middle_sum ((Re f),Si)) . k proof let k be Element of NAT ; ::_thesis: rseqi . k = (middle_sum ((Re f),Si)) . k consider H, z being FinSequence such that A26: H = T . k and A27: z = S . k and A28: len H = len z and A29: for j being Element of NAT st j in dom H holds ex rji being Element of COMPLEX ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A16; A30: dom (Re (S . k)) = dom (S . k) by COMSEQ_3:def_3 .= Seg (len H) by A27, A28, FINSEQ_1:def_3 .= Seg (len (Si . k)) by A26, INTEGR15:def_1 .= dom (Si . k) by FINSEQ_1:def_3 ; A31: for j being Nat st j in dom (Re (S . k)) holds (Re (S . k)) . j = (Si . k) . j proof let j0 be Nat; ::_thesis: ( j0 in dom (Re (S . k)) implies (Re (S . k)) . j0 = (Si . k) . j0 ) reconsider j = j0 as Element of NAT by ORDINAL1:def_12; assume A32: j0 in dom (Re (S . k)) ; ::_thesis: (Re (S . k)) . j0 = (Si . k) . j0 then j0 in Seg (len (Si . k)) by A30, FINSEQ_1:def_3; then j0 in Seg (len H) by A26, INTEGR15:def_1; then j in dom H by FINSEQ_1:def_3; then consider rji being Element of COMPLEX , tji being Element of REAL such that A33: tji in dom (f | (divset ((T . k),j))) and A34: (Si . k) . j = (vol (divset ((T . k),j))) * (((Re f) | (divset ((T . k),j))) . tji) and A35: rji = (f | (divset ((T . k),j))) . tji and A36: z . j = (vol (divset ((T . k),j))) * rji by A29; A37: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61 .= (dom (Re f)) /\ (divset ((T . k),j)) by COMSEQ_3:def_3 .= dom ((Re f) | (divset ((T . k),j))) by RELAT_1:61 ; then tji in (dom (Re f)) /\ (divset ((T . k),j)) by A33, RELAT_1:61; then A38: tji in dom (Re f) by XBOOLE_0:def_4; A39: ((Re f) | (divset ((T . k),j))) . tji = (Re f) . tji by A33, A37, FUNCT_1:47 .= Re (f . tji) by A38, COMSEQ_3:def_3 .= Re rji by A33, A35, FUNCT_1:47 ; (Re (S . k)) . j = Re ((S . k) . j) by A32, COMSEQ_3:def_3 .= (Si . k) . j by A34, A39, Th1, A27, A36 ; hence (Re (S . k)) . j0 = (Si . k) . j0 ; ::_thesis: verum end; A40: for j0 being set st j0 in dom (Re (S . k)) holds (Re (S . k)) . j0 = (Si . k) . j0 by A31; thus rseqi . k = Re (xseq . k) by COMSEQ_3:def_5 .= Re (middle_sum (f,(S . k))) by Def4 .= middle_sum ((Re f),(Si . k)) by A30, A40, Th7, FUNCT_1:2 .= (middle_sum ((Re f),Si)) . k by INTEGR15:def_4 ; ::_thesis: verum end; hence ( middle_sum ((Re f),Si) is convergent & lim (middle_sum ((Re f),Si)) = Ii ) by A25, FUNCT_2:63; ::_thesis: verum end; Re f is bounded by A1, Th13; then A41: Re f is integrable by A4, INTEGR15:10; A42: now__::_thesis:_for_T_being_DivSequence_of_A for_Si_being_middle_volume_Sequence_of_Im_f,T_st_delta_T_is_convergent_&_lim_(delta_T)_=_0_holds_ (_middle_sum_((Im_f),Si)_is_convergent_&_lim_(middle_sum_((Im_f),Si))_=_Ic_) set x = I; let T be DivSequence of A; ::_thesis: for Si being middle_volume_Sequence of Im f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic ) let Si be middle_volume_Sequence of Im f,T; ::_thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic ) ) defpred S1[ Element of NAT , set ] means ex H, z being FinSequence st ( H = T . \$1 & z = \$2 & len z = len H & ( for j being Element of NAT st j in dom H holds ex rji being Element of COMPLEX ex tji being Element of REAL st ( tji in dom (f | (divset ((T . \$1),j))) & (Si . \$1) . j = (vol (divset ((T . \$1),j))) * (((Im f) | (divset ((T . \$1),j))) . tji) & rji = (f | (divset ((T . \$1),j))) . tji & z . j = (vol (divset ((T . \$1),j))) * rji ) ) ); reconsider xs = I as Element of COMPLEX ; A43: for k being Element of NAT ex y being Element of COMPLEX * st S1[k,y] proof let k be Element of NAT ; ::_thesis: ex y being Element of COMPLEX * st S1[k,y] reconsider Tk = T . k as FinSequence ; defpred S2[ Nat, set ] means ex j being Element of NAT st ( \$1 = j & ex rji being Element of COMPLEX ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & \$2 = (vol (divset ((T . k),j))) * rji ) ); A44: for j being Nat st j in Seg (len Tk) holds ex x being Element of COMPLEX st S2[j,x] proof let j0 be Nat; ::_thesis: ( j0 in Seg (len Tk) implies ex x being Element of COMPLEX st S2[j0,x] ) assume A45: j0 in Seg (len Tk) ; ::_thesis: ex x being Element of COMPLEX st S2[j0,x] then reconsider j = j0 as Element of NAT ; j in dom Tk by A45, FINSEQ_1:def_3; then consider r being Element of REAL such that A46: r in rng ((Im f) | (divset ((T . k),j))) and A47: (Si . k) . j = r * (vol (divset ((T . k),j))) by INTEGR15:def_1; consider tji being set such that A48: tji in dom ((Im f) | (divset ((T . k),j))) and A49: r = ((Im f) | (divset ((T . k),j))) . tji by A46, FUNCT_1:def_3; tji in (dom (Im f)) /\ (divset ((T . k),j)) by A48, RELAT_1:61; then reconsider tji = tji as Element of REAL ; A50: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61 .= (dom (Im f)) /\ (divset ((T . k),j)) by COMSEQ_3:def_4 .= dom ((Im f) | (divset ((T . k),j))) by RELAT_1:61 ; then (f | (divset ((T . k),j))) . tji in rng (f | (divset ((T . k),j))) by A48, FUNCT_1:3; then reconsider rji = (f | (divset ((T . k),j))) . tji as Element of COMPLEX ; reconsider x = (vol (divset ((T . k),j))) * rji as Element of COMPLEX ; take x ; ::_thesis: S2[j0,x] thus S2[j0,x] by A47, A48, A49, A50; ::_thesis: verum end; consider p being FinSequence of COMPLEX such that A51: ( dom p = Seg (len Tk) & ( for j being Nat st j in Seg (len Tk) holds S2[j,p . j] ) ) from FINSEQ_1:sch_5(A44); reconsider x = p as Element of COMPLEX * by FINSEQ_1:def_11; take x ; ::_thesis: S1[k,x] A52: now__::_thesis:_for_jj0_being_Element_of_NAT_st_jj0_in_dom_Tk_holds_ ex_rji_being_Element_of_COMPLEX_ex_tji_being_Element_of_REAL_st_ (_tji_in_dom_(f_|_(divset_((T_._k),jj0)))_&_(Si_._k)_._jj0_=_(vol_(divset_((T_._k),jj0)))_*_(((Im_f)_|_(divset_((T_._k),jj0)))_._tji)_&_rji_=_(f_|_(divset_((T_._k),jj0)))_._tji_&_p_._jj0_=_(vol_(divset_((T_._k),jj0)))_*_rji_) let jj0 be Element of NAT ; ::_thesis: ( jj0 in dom Tk implies ex rji being Element of COMPLEX ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Im f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji ) ) reconsider j0 = jj0 as Nat ; A53: dom Tk = Seg (len Tk) by FINSEQ_1:def_3; assume jj0 in dom Tk ; ::_thesis: ex rji being Element of COMPLEX ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Im f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji ) then S2[j0,p . j0] by A51, A53; hence ex rji being Element of COMPLEX ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),jj0))) & (Si . k) . jj0 = (vol (divset ((T . k),jj0))) * (((Im f) | (divset ((T . k),jj0))) . tji) & rji = (f | (divset ((T . k),jj0))) . tji & p . jj0 = (vol (divset ((T . k),jj0))) * rji ) ; ::_thesis: verum end; len p = len Tk by A51, FINSEQ_1:def_3; hence S1[k,x] by A52; ::_thesis: verum end; consider S being Function of NAT,(COMPLEX *) such that A54: for x being Element of NAT holds S1[x,S . x] from FUNCT_2:sch_3(A43); for k being Element of NAT holds S . k is middle_volume of f,T . k proof let k be Element of NAT ; ::_thesis: S . k is middle_volume of f,T . k consider H, z being FinSequence such that A55: ( H = T . k & z = S . k & len H = len z ) and A56: for j being Element of NAT st j in dom H holds ex rji being Element of COMPLEX ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A54; A57: now__::_thesis:_for_x_being_Nat_st_x_in_dom_H_holds_ ex_rji_being_Element_of_COMPLEX_st_ (_rji_in_rng_(f_|_(divset_((T_._k),x)))_&_z_._x_=_rji_*_(vol_(divset_((T_._k),x)))_) let x be Nat; ::_thesis: ( x in dom H implies ex rji being Element of COMPLEX st ( rji in rng (f | (divset ((T . k),x))) & z . x = rji * (vol (divset ((T . k),x))) ) ) assume A58: x in dom H ; ::_thesis: ex rji being Element of COMPLEX st ( rji in rng (f | (divset ((T . k),x))) & z . x = rji * (vol (divset ((T . k),x))) ) then reconsider j = x as Element of NAT ; consider rji being Element of COMPLEX , tji being Element of REAL such that A59: tji in dom (f | (divset ((T . k),j))) and (Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) and A60: rji = (f | (divset ((T . k),j))) . tji and A61: z . j = (vol (divset ((T . k),j))) * rji by A56, A58; take rji = rji; ::_thesis: ( rji in rng (f | (divset ((T . k),x))) & z . x = rji * (vol (divset ((T . k),x))) ) thus rji in rng (f | (divset ((T . k),x))) by A59, A60, FUNCT_1:3; ::_thesis: z . x = rji * (vol (divset ((T . k),x))) thus z . x = rji * (vol (divset ((T . k),x))) by A61; ::_thesis: verum end; S . k is FinSequence of COMPLEX by FINSEQ_1:def_11; hence S . k is middle_volume of f,T . k by A55, A57, Def1; ::_thesis: verum end; then reconsider S = S as middle_volume_Sequence of f,T by Def3; set seq = middle_sum (f,S); reconsider xseq = middle_sum (f,S) as Function of NAT,COMPLEX ; assume ( delta T is convergent & lim (delta T) = 0 ) ; ::_thesis: ( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic ) then A62: ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) by A3; reconsider rseqi = Im (middle_sum (f,S)) as Real_Sequence ; A63: for k being Element of NAT holds ( rseqi . k = Im (xseq . k) & rseqi is convergent & Im xs = lim rseqi ) by A62, COMSEQ_3:41, COMSEQ_3:def_6; for k being Element of NAT holds rseqi . k = (middle_sum ((Im f),Si)) . k proof let k be Element of NAT ; ::_thesis: rseqi . k = (middle_sum ((Im f),Si)) . k consider H, z being FinSequence such that A64: H = T . k and A65: z = S . k and A66: len H = len z and A67: for j being Element of NAT st j in dom H holds ex rji being Element of COMPLEX ex tji being Element of REAL st ( tji in dom (f | (divset ((T . k),j))) & (Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) & rji = (f | (divset ((T . k),j))) . tji & z . j = (vol (divset ((T . k),j))) * rji ) by A54; A68: dom (Im (S . k)) = dom (S . k) by COMSEQ_3:def_4 .= Seg (len H) by A65, A66, FINSEQ_1:def_3 .= Seg (len (Si . k)) by A64, INTEGR15:def_1 .= dom (Si . k) by FINSEQ_1:def_3 ; A69: for j being Nat st j in dom (Im (S . k)) holds (Im (S . k)) . j = (Si . k) . j proof let j0 be Nat; ::_thesis: ( j0 in dom (Im (S . k)) implies (Im (S . k)) . j0 = (Si . k) . j0 ) reconsider j = j0 as Element of NAT by ORDINAL1:def_12; assume A70: j0 in dom (Im (S . k)) ; ::_thesis: (Im (S . k)) . j0 = (Si . k) . j0 then j0 in Seg (len (Si . k)) by A68, FINSEQ_1:def_3; then j0 in Seg (len H) by A64, INTEGR15:def_1; then j in dom H by FINSEQ_1:def_3; then consider rji being Element of COMPLEX , tji being Element of REAL such that A71: tji in dom (f | (divset ((T . k),j))) and A72: (Si . k) . j = (vol (divset ((T . k),j))) * (((Im f) | (divset ((T . k),j))) . tji) and A73: rji = (f | (divset ((T . k),j))) . tji and A74: z . j = (vol (divset ((T . k),j))) * rji by A67; A75: dom (f | (divset ((T . k),j))) = (dom f) /\ (divset ((T . k),j)) by RELAT_1:61 .= (dom (Im f)) /\ (divset ((T . k),j)) by COMSEQ_3:def_4 .= dom ((Im f) | (divset ((T . k),j))) by RELAT_1:61 ; then tji in (dom (Im f)) /\ (divset ((T . k),j)) by A71, RELAT_1:61; then A76: tji in dom (Im f) by XBOOLE_0:def_4; A77: ((Im f) | (divset ((T . k),j))) . tji = (Im f) . tji by A71, A75, FUNCT_1:47 .= Im (f . tji) by A76, COMSEQ_3:def_4 .= Im rji by A71, A73, FUNCT_1:47 ; (Im (S . k)) . j = Im ((S . k) . j) by A70, COMSEQ_3:def_4 .= (Si . k) . j by A72, A77, A65, A74, Th1 ; hence (Im (S . k)) . j0 = (Si . k) . j0 ; ::_thesis: verum end; A78: for j0 being set st j0 in dom (Im (S . k)) holds (Im (S . k)) . j0 = (Si . k) . j0 by A69; thus rseqi . k = Im (xseq . k) by COMSEQ_3:def_6 .= Im (middle_sum (f,(S . k))) by Def4 .= middle_sum ((Im f),(Si . k)) by A78, A68, Th8, FUNCT_1:2 .= (middle_sum ((Im f),Si)) . k by INTEGR15:def_4 ; ::_thesis: verum end; hence ( middle_sum ((Im f),Si) is convergent & lim (middle_sum ((Im f),Si)) = Ic ) by A63, FUNCT_2:63; ::_thesis: verum end; Im f is bounded by A1, Th13; then Im f is integrable by A42, INTEGR15:10; hence f is integrable by A41, Def5; ::_thesis: verum end; hence ( ex I being Element of COMPLEX st for T being DivSequence of A for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds ( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) implies f is integrable ) ; ::_thesis: verum end; definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of REAL,COMPLEX; predf is_integrable_on A means :Def7: :: INTEGR16:def 7 ( Re f is_integrable_on A & Im f is_integrable_on A ); end; :: deftheorem Def7 defines is_integrable_on INTEGR16:def_7_:_ for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,COMPLEX holds ( f is_integrable_on A iff ( Re f is_integrable_on A & Im f is_integrable_on A ) ); definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of REAL,COMPLEX; func integral (f,A) -> Element of COMPLEX equals :: INTEGR16:def 8 (integral ((Re f),A)) + ((integral ((Im f),A)) * ); correctness coherence (integral ((Re f),A)) + ((integral ((Im f),A)) * ) is Element of COMPLEX ; ; end; :: deftheorem defines integral INTEGR16:def_8_:_ for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,COMPLEX holds integral (f,A) = (integral ((Re f),A)) + ((integral ((Im f),A)) * ); Lm4: for f being PartFunc of REAL,COMPLEX for A being Subset of REAL holds ( Re (f | A) = (Re f) | A & Im (f | A) = (Im f) | A ) proof let f be PartFunc of REAL,COMPLEX; ::_thesis: for A being Subset of REAL holds ( Re (f | A) = (Re f) | A & Im (f | A) = (Im f) | A ) let A be Subset of REAL; ::_thesis: ( Re (f | A) = (Re f) | A & Im (f | A) = (Im f) | A ) dom ((Re f) | A) = (dom (Re f)) /\ A by RELAT_1:61 .= (dom f) /\ A by COMSEQ_3:def_3 ; then A1: dom ((Re f) | A) = dom (f | A) by RELAT_1:61 .= dom (Re (f | A)) by COMSEQ_3:def_3 ; now__::_thesis:_for_x_being_set_st_x_in_dom_((Re_f)_|_A)_holds_ (Re_(f_|_A))_._x_=_((Re_f)_|_A)_._x let x be set ; ::_thesis: ( x in dom ((Re f) | A) implies (Re (f | A)) . x = ((Re f) | A) . x ) assume A2: x in dom ((Re f) | A) ; ::_thesis: (Re (f | A)) . x = ((Re f) | A) . x then A3: x in (dom (Re f)) /\ A by RELAT_1:61; then A4: x in dom (Re f) by XBOOLE_0:def_4; A5: x in A by A3, XBOOLE_0:def_4; thus (Re (f | A)) . x = Re ((f | A) . x) by A1, A2, COMSEQ_3:def_3 .= Re (f . x) by A5, FUNCT_1:49 .= (Re f) . x by A4, COMSEQ_3:def_3 .= ((Re f) | A) . x by A5, FUNCT_1:49 ; ::_thesis: verum end; hence (Re f) | A = Re (f | A) by A1, FUNCT_1:2; ::_thesis: Im (f | A) = (Im f) | A dom ((Im f) | A) = (dom (Im f)) /\ A by RELAT_1:61 .= (dom f) /\ A by COMSEQ_3:def_4 ; then A6: dom ((Im f) | A) = dom (f | A) by RELAT_1:61 .= dom (Im (f | A)) by COMSEQ_3:def_4 ; now__::_thesis:_for_x_being_set_st_x_in_dom_((Im_f)_|_A)_holds_ (Im_(f_|_A))_._x_=_((Im_f)_|_A)_._x let x be set ; ::_thesis: ( x in dom ((Im f) | A) implies (Im (f | A)) . x = ((Im f) | A) . x ) assume A7: x in dom ((Im f) | A) ; ::_thesis: (Im (f | A)) . x = ((Im f) | A) . x then A8: x in (dom (Im f)) /\ A by RELAT_1:61; then A9: x in dom (Im f) by XBOOLE_0:def_4; A10: x in A by A8, XBOOLE_0:def_4; thus (Im (f | A)) . x = Im ((f | A) . x) by A6, A7, COMSEQ_3:def_4 .= Im (f . x) by A10, FUNCT_1:49 .= (Im f) . x by A9, COMSEQ_3:def_4 .= ((Im f) | A) . x by A10, FUNCT_1:49 ; ::_thesis: verum end; hence Im (f | A) = (Im f) | A by A6, FUNCT_1:2; ::_thesis: verum end; theorem :: INTEGR16:16 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,COMPLEX for g being Function of A,COMPLEX st f | A = g holds ( f is_integrable_on A iff g is integrable ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,COMPLEX for g being Function of A,COMPLEX st f | A = g holds ( f is_integrable_on A iff g is integrable ) let f be PartFunc of REAL,COMPLEX; ::_thesis: for g being Function of A,COMPLEX st f | A = g holds ( f is_integrable_on A iff g is integrable ) let g be Function of A,COMPLEX; ::_thesis: ( f | A = g implies ( f is_integrable_on A iff g is integrable ) ) assume A1: f | A = g ; ::_thesis: ( f is_integrable_on A iff g is integrable ) thus ( f is_integrable_on A implies g is integrable ) ::_thesis: ( g is integrable implies f is_integrable_on A ) proof assume A2: f is_integrable_on A ; ::_thesis: g is integrable ( Re g is integrable & Im g is integrable ) proof A3: A = dom g by FUNCT_2:def_1 .= (dom f) /\ A by A1, RELAT_1:61 ; then A = (dom (Re f)) /\ A by COMSEQ_3:def_3; then (Re f) || A is total by INTEGRA5:6, XBOOLE_1:17; then reconsider F = (Re f) | A as Function of A,REAL ; A4: Re f is_integrable_on A by A2, Def7; dom g = A by FUNCT_2:def_1; then reconsider g0 = g as PartFunc of REAL,COMPLEX by RELSET_1:5; Re g = Re g0 .= F by A1, Lm4 ; hence Re g is integrable by A4, INTEGRA5:def_1; ::_thesis: Im g is integrable A = (dom (Im f)) /\ A by A3, COMSEQ_3:def_4; then (Im f) || A is total by INTEGRA5:6, XBOOLE_1:17; then reconsider G = (Im f) | A as Function of A,REAL ; A5: Im f is_integrable_on A by A2, Def7; Im g = Im g0 .= G by A1, Lm4 ; hence Im g is integrable by A5, INTEGRA5:def_1; ::_thesis: verum end; hence g is integrable by Def5; ::_thesis: verum end; assume A6: g is integrable ; ::_thesis: f is_integrable_on A ( Re f is_integrable_on A & Im f is_integrable_on A ) proof dom g = A by FUNCT_2:def_1; then reconsider g0 = g as PartFunc of REAL,COMPLEX by RELSET_1:5; Re g = Re g0 .= (Re f) || A by A1, Lm4 ; then (Re f) || A is integrable by A6, Def5; hence Re f is_integrable_on A by INTEGRA5:def_1; ::_thesis: Im f is_integrable_on A Im g = Im g0 .= (Im f) || A by A1, Lm4 ; then (Im f) || A is integrable by A6, Def5; hence Im f is_integrable_on A by INTEGRA5:def_1; ::_thesis: verum end; hence f is_integrable_on A by Def7; ::_thesis: verum end; theorem :: INTEGR16:17 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,COMPLEX for g being Function of A,COMPLEX st f | A = g holds integral (f,A) = integral g proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,COMPLEX for g being Function of A,COMPLEX st f | A = g holds integral (f,A) = integral g let f be PartFunc of REAL,COMPLEX; ::_thesis: for g being Function of A,COMPLEX st f | A = g holds integral (f,A) = integral g let g be Function of A,COMPLEX; ::_thesis: ( f | A = g implies integral (f,A) = integral g ) assume A1: f | A = g ; ::_thesis: integral (f,A) = integral g A2: A = dom g by FUNCT_2:def_1 .= (dom f) /\ A by A1, RELAT_1:61 ; then A = (dom (Re f)) /\ A by COMSEQ_3:def_3; then (Re f) || A is total by INTEGRA5:6, XBOOLE_1:17; then reconsider F = (Re f) | A as Function of A,REAL ; dom g = A by FUNCT_2:def_1; then reconsider g0 = g as PartFunc of REAL,COMPLEX by RELSET_1:5; A3: Re g = Re g0 .= F by A1, Lm4 ; A = (dom (Im f)) /\ A by A2, COMSEQ_3:def_4; then (Im f) || A is total by INTEGRA5:6, XBOOLE_1:17; then reconsider G = (Im f) | A as Function of A,REAL ; Im g = Im g0 .= G by A1, Lm4 ; hence integral (f,A) = integral g by A3; ::_thesis: verum end; definition let a, b be real number ; let f be PartFunc of REAL,COMPLEX; func integral (f,a,b) -> Element of COMPLEX equals :: INTEGR16:def 9 (integral ((Re f),a,b)) + ((integral ((Im f),a,b)) * ); correctness coherence (integral ((Re f),a,b)) + ((integral ((Im f),a,b)) * ) is Element of COMPLEX ; ; end; :: deftheorem defines integral INTEGR16:def_9_:_ for a, b being real number for f being PartFunc of REAL,COMPLEX holds integral (f,a,b) = (integral ((Re f),a,b)) + ((integral ((Im f),a,b)) * ); begin theorem Th18: :: INTEGR16:18 for c being complex number for f being PartFunc of REAL,COMPLEX holds ( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Re c) (#) (Im f)) + ((Im c) (#) (Re f)) ) proof let c be complex number ; ::_thesis: for f being PartFunc of REAL,COMPLEX holds ( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Re c) (#) (Im f)) + ((Im c) (#) (Re f)) ) let f be PartFunc of REAL,COMPLEX; ::_thesis: ( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Re c) (#) (Im f)) + ((Im c) (#) (Re f)) ) A1: dom (Re (c (#) f)) = dom (c (#) f) by COMSEQ_3:def_3 .= dom f by VALUED_1:def_5 ; A2: dom (Im (c (#) f)) = dom (c (#) f) by COMSEQ_3:def_4 .= dom f by VALUED_1:def_5 ; A3: dom ((Re c) (#) (Re f)) = dom (Re f) by VALUED_1:def_5 .= dom f by COMSEQ_3:def_3 ; A4: dom ((Im c) (#) (Im f)) = dom (Im f) by VALUED_1:def_5 .= dom f by COMSEQ_3:def_4 ; A5: dom ((Im c) (#) (Re f)) = dom (Re f) by VALUED_1:def_5 .= dom f by COMSEQ_3:def_3 ; A6: dom ((Re c) (#) (Im f)) = dom (Im f) by VALUED_1:def_5 .= dom f by COMSEQ_3:def_4 ; A7: dom (Re (c (#) f)) = (dom f) /\ (dom f) by A1 .= dom (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) by A3, A4, VALUED_1:12 ; A8: dom (Im (c (#) f)) = (dom f) /\ (dom f) by A2 .= dom (((Re c) (#) (Im f)) + ((Im c) (#) (Re f))) by A5, A6, VALUED_1:def_1 ; now__::_thesis:_for_x_being_set_st_x_in_dom_(Re_(c_(#)_f))_holds_ (Re_(c_(#)_f))_._x_=_(((Re_c)_(#)_(Re_f))_-_((Im_c)_(#)_(Im_f)))_._x let x be set ; ::_thesis: ( x in dom (Re (c (#) f)) implies (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x ) assume A9: x in dom (Re (c (#) f)) ; ::_thesis: (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x then A10: ( x in dom (Re f) & x in dom (Im f) ) by A1, COMSEQ_3:def_3, COMSEQ_3:def_4; thus (Re (c (#) f)) . x = Re ((c (#) f) . x) by A9, COMSEQ_3:def_3 .= Re (c * (f . x)) by VALUED_1:6 .= ((Re c) * (Re (f . x))) - ((Im c) * (Im (f . x))) by COMPLEX1:9 .= ((Re c) * ((Re f) . x)) - ((Im c) * (Im (f . x))) by A10, COMSEQ_3:def_3 .= ((Re c) * ((Re f) . x)) - ((Im c) * ((Im f) . x)) by A10, COMSEQ_3:def_4 .= (((Re c) (#) (Re f)) . x) - ((Im c) * ((Im f) . x)) by VALUED_1:6 .= (((Re c) (#) (Re f)) . x) - (((Im c) (#) (Im f)) . x) by VALUED_1:6 .= (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x by A9, A7, VALUED_1:13 ; ::_thesis: verum end; hence Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) by A7, FUNCT_1:2; ::_thesis: Im (c (#) f) = ((Re c) (#) (Im f)) + ((Im c) (#) (Re f)) now__::_thesis:_for_x_being_set_st_x_in_dom_(Im_(c_(#)_f))_holds_ (Im_(c_(#)_f))_._x_=_(((Re_c)_(#)_(Im_f))_+_((Im_c)_(#)_(Re_f)))_._x let x be set ; ::_thesis: ( x in dom (Im (c (#) f)) implies (Im (c (#) f)) . x = (((Re c) (#) (Im f)) + ((Im c) (#) (Re f))) . x ) assume A11: x in dom (Im (c (#) f)) ; ::_thesis: (Im (c (#) f)) . x = (((Re c) (#) (Im f)) + ((Im c) (#) (Re f))) . x then A12: ( x in dom (Re f) & x in dom (Im f) ) by A2, COMSEQ_3:def_3, COMSEQ_3:def_4; thus (Im (c (#) f)) . x = Im ((c (#) f) . x) by A11, COMSEQ_3:def_4 .= Im (c * (f . x)) by VALUED_1:6 .= ((Re c) * (Im (f . x))) + ((Im c) * (Re (f . x))) by COMPLEX1:9 .= ((Re c) * ((Im f) . x)) + ((Im c) * (Re (f . x))) by A12, COMSEQ_3:def_4 .= ((Re c) * ((Im f) . x)) + ((Im c) * ((Re f) . x)) by A12, COMSEQ_3:def_3 .= (((Re c) (#) (Im f)) . x) + ((Im c) * ((Re f) . x)) by VALUED_1:6 .= (((Re c) (#) (Im f)) . x) + (((Im c) (#) (Re f)) . x) by VALUED_1:6 .= (((Re c) (#) (Im f)) + ((Im c) (#) (Re f))) . x by A11, A8, VALUED_1:def_1 ; ::_thesis: verum end; hence Im (c (#) f) = ((Re c) (#) (Im f)) + ((Im c) (#) (Re f)) by A8, FUNCT_1:2; ::_thesis: verum end; theorem :: INTEGR16:19 for A being non empty closed_interval Subset of REAL for f1, f2 being PartFunc of REAL,COMPLEX st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,COMPLEX st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) let f1, f2 be PartFunc of REAL,COMPLEX; ::_thesis: ( f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded implies ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) ) assume that A1: ( f1 is_integrable_on A & f2 is_integrable_on A ) and A2: ( A c= dom f1 & A c= dom f2 ) and A3: f1 | A is bounded and A4: f2 | A is bounded ; ::_thesis: ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) A5: ( (Re f1) + (Re f2) is_integrable_on A & (Im f1) + (Im f2) is_integrable_on A & integral (((Re f1) + (Re f2)),A) = (integral ((Re f1),A)) + (integral ((Re f2),A)) & integral (((Im f1) + (Im f2)),A) = (integral ((Im f1),A)) + (integral ((Im f2),A)) & (Re f1) - (Re f2) is_integrable_on A & (Im f1) - (Im f2) is_integrable_on A & integral (((Re f1) - (Re f2)),A) = (integral ((Re f1),A)) - (integral ((Re f2),A)) & integral (((Im f1) - (Im f2)),A) = (integral ((Im f1),A)) - (integral ((Im f2),A)) ) proof A6: ( A c= dom (Re f1) & A c= dom (Re f2) & A c= dom (Im f1) & A c= dom (Im f2) ) by A2, COMSEQ_3:def_3, COMSEQ_3:def_4; ( Re (f2 | A) is bounded & Im (f2 | A) is bounded ) by A4, Th11; then A7: ( (Re f2) | A is bounded & (Im f2) | A is bounded ) by Lm4; ( Re (f1 | A) is bounded & Im (f1 | A) is bounded ) by A3, Th11; then A8: ( (Re f1) | A is bounded & (Im f1) | A is bounded ) by Lm4; A9: ( Re f1 is_integrable_on A & Im f1 is_integrable_on A & Re f2 is_integrable_on A & Im f2 is_integrable_on A ) by A1, Def7; hence ( (Re f1) + (Re f2) is_integrable_on A & (Im f1) + (Im f2) is_integrable_on A & integral (((Re f1) + (Re f2)),A) = (integral ((Re f1),A)) + (integral ((Re f2),A)) & integral (((Im f1) + (Im f2)),A) = (integral ((Im f1),A)) + (integral ((Im f2),A)) ) by A6, A7, A8, INTEGRA6:11; ::_thesis: ( (Re f1) - (Re f2) is_integrable_on A & (Im f1) - (Im f2) is_integrable_on A & integral (((Re f1) - (Re f2)),A) = (integral ((Re f1),A)) - (integral ((Re f2),A)) & integral (((Im f1) - (Im f2)),A) = (integral ((Im f1),A)) - (integral ((Im f2),A)) ) thus ( (Re f1) - (Re f2) is_integrable_on A & (Im f1) - (Im f2) is_integrable_on A & integral (((Re f1) - (Re f2)),A) = (integral ((Re f1),A)) - (integral ((Re f2),A)) & integral (((Im f1) - (Im f2)),A) = (integral ((Im f1),A)) - (integral ((Im f2),A)) ) by A6, A7, A8, A9, INTEGRA6:11; ::_thesis: verum end; then ( Re (f1 + f2) is_integrable_on A & Im (f1 + f2) is_integrable_on A & Re (f1 - f2) is_integrable_on A & Im (f1 - f2) is_integrable_on A ) by MESFUN6C:5, MESFUN6C:6; hence ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A ) by Def7; ::_thesis: ( integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) & integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ) ( (Re (integral (f1,A))) + (Re (integral (f2,A))) = (integral ((Re f1),A)) + (integral ((Re f2),A)) & (Im (integral (f1,A))) + (Im (integral (f2,A))) = (integral ((Im f1),A)) + (integral ((Im f2),A)) & (Re (integral (f1,A))) - (Re (integral (f2,A))) = (integral ((Re f1),A)) - (integral ((Re f2),A)) & (Im (integral (f1,A))) - (Im (integral (f2,A))) = (integral ((Im f1),A)) - (integral ((Im f2),A)) ) proof ( Re (integral (f1,A)) = integral ((Re f1),A) & Im (integral (f1,A)) = integral ((Im f1),A) & Re (integral (f2,A)) = integral ((Re f2),A) & Im (integral (f2,A)) = integral ((Im f2),A) ) by COMPLEX1:12; hence ( (Re (integral (f1,A))) + (Re (integral (f2,A))) = (integral ((Re f1),A)) + (integral ((Re f2),A)) & (Im (integral (f1,A))) + (Im (integral (f2,A))) = (integral ((Im f1),A)) + (integral ((Im f2),A)) & (Re (integral (f1,A))) - (Re (integral (f2,A))) = (integral ((Re f1),A)) - (integral ((Re f2),A)) & (Im (integral (f1,A))) - (Im (integral (f2,A))) = (integral ((Im f1),A)) - (integral ((Im f2),A)) ) ; ::_thesis: verum end; then ( (Re (integral (f1,A))) + (Re (integral (f2,A))) = integral ((Re (f1 + f2)),A) & (Im (integral (f1,A))) + (Im (integral (f2,A))) = integral ((Im (f1 + f2)),A) & (Re (integral (f1,A))) - (Re (integral (f2,A))) = integral ((Re (f1 - f2)),A) & (Im (integral (f1,A))) - (Im (integral (f2,A))) = integral ((Im (f1 - f2)),A) ) by A5, MESFUN6C:5, MESFUN6C:6; then A10: ( Re (integral ((f1 + f2),A)) = (Re (integral (f1,A))) + (Re (integral (f2,A))) & Im (integral ((f1 + f2),A)) = (Im (integral (f1,A))) + (Im (integral (f2,A))) & Re (integral ((f1 - f2),A)) = (Re (integral (f1,A))) - (Re (integral (f2,A))) & Im (integral ((f1 - f2),A)) = (Im (integral (f1,A))) - (Im (integral (f2,A))) ) by COMPLEX1:12; then ( Re (integral ((f1 + f2),A)) = Re ((integral (f1,A)) + (integral (f2,A))) & Im (integral ((f1 + f2),A)) = Im ((integral (f1,A)) + (integral (f2,A))) ) by COMPLEX1:8; hence integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) by COMPLEX1:def_3; ::_thesis: integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) ( Re (integral ((f1 - f2),A)) = Re ((integral (f1,A)) - (integral (f2,A))) & Im (integral ((f1 - f2),A)) = Im ((integral (f1,A)) - (integral (f2,A))) ) by A10, COMPLEX1:19; hence integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) by COMPLEX1:def_3; ::_thesis: verum end; theorem :: INTEGR16:20 for r being Real for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,COMPLEX st A c= dom f & f is_integrable_on A & f | A is bounded holds ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) proof let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,COMPLEX st A c= dom f & f is_integrable_on A & f | A is bounded holds ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,COMPLEX st A c= dom f & f is_integrable_on A & f | A is bounded holds ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) let f be PartFunc of REAL,COMPLEX; ::_thesis: ( A c= dom f & f is_integrable_on A & f | A is bounded implies ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) ) assume that A1: A c= dom f and A2: f is_integrable_on A and A3: f | A is bounded ; ::_thesis: ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) A4: ( Re f is_integrable_on A & Im f is_integrable_on A ) by A2, Def7; A5: ( integral ((r (#) (Re f)),A) = r * (integral ((Re f),A)) & integral ((r (#) (Im f)),A) = r * (integral ((Im f),A)) ) proof ( Re (f | A) is bounded & Im (f | A) is bounded ) by A3, Th11; then A6: ( (Re f) | A is bounded & (Im f) | A is bounded ) by Lm4; A7: ( A c= dom (Re f) & A c= dom (Im f) ) by A1, COMSEQ_3:def_3, COMSEQ_3:def_4; hence integral ((r (#) (Re f)),A) = r * (integral ((Re f),A)) by A4, A6, INTEGRA6:9; ::_thesis: integral ((r (#) (Im f)),A) = r * (integral ((Im f),A)) thus integral ((r (#) (Im f)),A) = r * (integral ((Im f),A)) by A4, A6, A7, INTEGRA6:9; ::_thesis: verum end; A8: ( Re (integral ((r (#) f),A)) = r * (Re (integral (f,A))) & Im (integral ((r (#) f),A)) = r * (Im (integral (f,A))) ) proof ( Re (integral ((r (#) f),A)) = integral ((Re (r (#) f)),A) & r * (Re (integral (f,A))) = r * (integral ((Re f),A)) & Im (integral ((r (#) f),A)) = integral ((Im (r (#) f)),A) & r * (Im (integral (f,A))) = r * (integral ((Im f),A)) ) by COMPLEX1:12; hence ( Re (integral ((r (#) f),A)) = r * (Re (integral (f,A))) & Im (integral ((r (#) f),A)) = r * (Im (integral (f,A))) ) by A5, MESFUN6C:2; ::_thesis: verum end; ( Re (r (#) f) is_integrable_on A & Im (r (#) f) is_integrable_on A ) proof ( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) ) by Lm4; then A9: ( (Re f) | A is bounded & (Im f) | A is bounded ) by A3, Th11; A10: ( A c= dom (Re f) & A c= dom (Im f) ) by A1, COMSEQ_3:def_3, COMSEQ_3:def_4; ( Re f is_integrable_on A & Im f is_integrable_on A ) by A2, Def7; then ( r (#) (Re f) is_integrable_on A & r (#) (Im f) is_integrable_on A ) by A9, A10, INTEGRA6:9; hence ( Re (r (#) f) is_integrable_on A & Im (r (#) f) is_integrable_on A ) by MESFUN6C:2; ::_thesis: verum end; hence r (#) f is_integrable_on A by Def7; ::_thesis: integral ((r (#) f),A) = r * (integral (f,A)) ( Re (integral ((r (#) f),A)) = Re (r * (integral (f,A))) & Im (integral ((r (#) f),A)) = Im (r * (integral (f,A))) ) by A8, Th1; hence integral ((r (#) f),A) = r * (integral (f,A)) by COMPLEX1:def_3; ::_thesis: verum end; theorem :: INTEGR16:21 for c being complex number for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,COMPLEX st A c= dom f & f is_integrable_on A & f | A is bounded holds ( c (#) f is_integrable_on A & integral ((c (#) f),A) = c * (integral (f,A)) ) proof let c be complex number ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,COMPLEX st A c= dom f & f is_integrable_on A & f | A is bounded holds ( c (#) f is_integrable_on A & integral ((c (#) f),A) = c * (integral (f,A)) ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being PartFunc of REAL,COMPLEX st A c= dom f & f is_integrable_on A & f | A is bounded holds ( c (#) f is_integrable_on A & integral ((c (#) f),A) = c * (integral (f,A)) ) let f be PartFunc of REAL,COMPLEX; ::_thesis: ( A c= dom f & f is_integrable_on A & f | A is bounded implies ( c (#) f is_integrable_on A & integral ((c (#) f),A) = c * (integral (f,A)) ) ) assume that A1: A c= dom f and A2: f is_integrable_on A and A3: f | A is bounded ; ::_thesis: ( c (#) f is_integrable_on A & integral ((c (#) f),A) = c * (integral (f,A)) ) A4: ( Re (c * (integral (f,A))) = ((Re c) * (integral ((Re f),A))) - ((Im c) * (integral ((Im f),A))) & Im (c * (integral (f,A))) = ((Re c) * (integral ((Im f),A))) + ((Im c) * (integral ((Re f),A))) ) proof A5: Re (integral (f,A)) = integral ((Re f),A) by COMPLEX1:12; A6: Im (integral (f,A)) = integral ((Im f),A) by COMPLEX1:12; hence Re (c * (integral (f,A))) = ((Re c) * (integral ((Re f),A))) - ((Im c) * (integral ((Im f),A))) by A5, COMPLEX1:9; ::_thesis: Im (c * (integral (f,A))) = ((Re c) * (integral ((Im f),A))) + ((Im c) * (integral ((Re f),A))) thus Im (c * (integral (f,A))) = ((Re c) * (integral ((Im f),A))) + ((Im c) * (integral ((Re f),A))) by A5, A6, COMPLEX1:9; ::_thesis: verum end; ( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) ) by Lm4; then A7: ( (Re f) | A is bounded & (Im f) | A is bounded ) by A3, Th11; A8: ( A c= dom (Re f) & A c= dom (Im f) ) by A1, COMSEQ_3:def_3, COMSEQ_3:def_4; A9: ( Re f is_integrable_on A & Im f is_integrable_on A ) by A2, Def7; then A10: ( (Re c) (#) (Re f) is_integrable_on A & (Re c) (#) (Im f) is_integrable_on A & (Im c) (#) (Re f) is_integrable_on A & (Im c) (#) (Im f) is_integrable_on A ) by A7, A8, INTEGRA6:9; A11: ( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Re c) (#) (Im f)) + ((Im c) (#) (Re f)) ) by Th18; A12: ( ((Re c) (#) (Re f)) | A is bounded & ((Re c) (#) (Im f)) | A is bounded & ((Im c) (#) (Re f)) | A is bounded & ((Im c) (#) (Im f)) | A is bounded ) by A7, RFUNCT_1:80; ( dom (Re f) = dom f & dom (Im f) = dom f ) by COMSEQ_3:def_3, COMSEQ_3:def_4; then A13: ( A c= dom ((Re c) (#) (Re f)) & A c= dom ((Re c) (#) (Im f)) & A c= dom ((Im c) (#) (Re f)) & A c= dom ((Im c) (#) (Im f)) ) by A1, VALUED_1:def_5; then A14: Re (c (#) f) is_integrable_on A by A10, A11, A12, INTEGRA6:11; Im (c (#) f) is_integrable_on A by A10, A11, A12, A13, INTEGRA6:11; hence c (#) f is_integrable_on A by A14, Def7; ::_thesis: integral ((c (#) f),A) = c * (integral (f,A)) A15: Re (integral ((c (#) f),A)) = integral ((Re (c (#) f)),A) by COMPLEX1:12 .= (integral (((Re c) (#) (Re f)),A)) - (integral (((Im c) (#) (Im f)),A)) by A10, A11, A12, A13, INTEGRA6:11 .= ((Re c) * (integral ((Re f),A))) - (integral (((Im c) (#) (Im f)),A)) by A9, A7, A8, INTEGRA6:9 .= Re (c * (integral (f,A))) by A4, A9, A7, A8, INTEGRA6:9 ; Im (integral ((c (#) f),A)) = integral ((Im (c (#) f)),A) by COMPLEX1:12 .= (integral (((Re c) (#) (Im f)),A)) + (integral (((Im c) (#) (Re f)),A)) by A10, A11, A12, A13, INTEGRA6:11 .= ((Re c) * (integral ((Im f),A))) + (integral (((Im c) (#) (Re f)),A)) by A9, A7, A8, INTEGRA6:9 .= Im (c * (integral (f,A))) by A4, A9, A7, A8, INTEGRA6:9 ; hence integral ((c (#) f),A) = c * (integral (f,A)) by A15, COMPLEX1:def_3; ::_thesis: verum end; theorem :: INTEGR16:22 for f being PartFunc of REAL,COMPLEX for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.a,b.] holds integral (f,A) = integral (f,a,b) proof let f be PartFunc of REAL,COMPLEX; ::_thesis: for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.a,b.] holds integral (f,A) = integral (f,a,b) let A be non empty closed_interval Subset of REAL; ::_thesis: for a, b being Real st A = [.a,b.] holds integral (f,A) = integral (f,a,b) let a, b be Real; ::_thesis: ( A = [.a,b.] implies integral (f,A) = integral (f,a,b) ) assume A1: A = [.a,b.] ; ::_thesis: integral (f,A) = integral (f,a,b) ( Re (integral (f,A)) = integral ((Re f),A) & Im (integral (f,A)) = integral ((Im f),A) & Re (integral (f,a,b)) = integral ((Re f),a,b) & Im (integral (f,a,b)) = integral ((Im f),a,b) ) by COMPLEX1:12; then ( Re (integral (f,A)) = Re (integral (f,a,b)) & Im (integral (f,A)) = Im (integral (f,a,b)) ) by A1, INTEGRA5:19; hence integral (f,A) = integral (f,a,b) by COMPLEX1:def_3; ::_thesis: verum end; theorem :: INTEGR16:23 for f being PartFunc of REAL,COMPLEX for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.b,a.] holds - (integral (f,A)) = integral (f,a,b) proof let f be PartFunc of REAL,COMPLEX; ::_thesis: for A being non empty closed_interval Subset of REAL for a, b being Real st A = [.b,a.] holds - (integral (f,A)) = integral (f,a,b) let A be non empty closed_interval Subset of REAL; ::_thesis: for a, b being Real st A = [.b,a.] holds - (integral (f,A)) = integral (f,a,b) let a, b be Real; ::_thesis: ( A = [.b,a.] implies - (integral (f,A)) = integral (f,a,b) ) assume A1: A = [.b,a.] ; ::_thesis: - (integral (f,A)) = integral (f,a,b) A2: ( Re (integral (f,a,b)) = integral ((Re f),a,b) & Im (integral (f,a,b)) = integral ((Im f),a,b) ) by COMPLEX1:12; A3: Re (- (integral (f,A))) = - (Re (integral (f,A))) by COMPLEX1:17 .= - (integral ((Re f),A)) by COMPLEX1:12 ; A4: Im (- (integral (f,A))) = - (Im (integral (f,A))) by COMPLEX1:17 .= - (integral ((Im f),A)) by COMPLEX1:12 ; A5: Re (- (integral (f,A))) = Re (integral (f,a,b)) by A3, A1, A2, INTEGRA5:20; Im (- (integral (f,A))) = Im (integral (f,a,b)) by A4, A1, A2, INTEGRA5:20; hence - (integral (f,A)) = integral (f,a,b) by A5, COMPLEX1:def_3; ::_thesis: verum end;