integr16.miz



    begin

    theorem :: INTEGR16:1

    

     Th1: for z be Complex, r be Real holds ( Re (r * z)) = (r * ( Re z)) & ( Im (r * z)) = (r * ( Im z))

    proof

      let z be Complex, r be Real;

      

       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 COMPLEX1:def 2

      .= (r * ( Re z));

      

      thus ( Im (r * z)) = ((r * ( Im z)) + (( Re z) * ( Im r))) by A2, COMPLEX1: 9

      .= ((r * ( Im z)) + ( 0 * ( Re z))) by COMPLEX1:def 2

      .= (r * ( Im z));

    end;

     Lm1:

    now

      let f be FinSequence, g be Function;

      ex n be 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;

    end;

    registration

      let S be FinSequence of COMPLEX ;

      cluster ( Re S) -> FinSequence-like;

      coherence

      proof

        ( dom ( Re S)) = ( dom S) by COMSEQ_3:def 3;

        hence thesis by Lm1;

      end;

      cluster ( Im S) -> FinSequence-like;

      coherence

      proof

        ( dom ( Im S)) = ( dom S) by COMSEQ_3:def 4;

        hence thesis by Lm1;

      end;

    end

    definition

      let S be FinSequence of COMPLEX ;

      :: original: Re

      redefine

      func Re S -> FinSequence of REAL ;

      coherence

      proof

        ( rng ( Re S)) c= REAL ;

        hence thesis by FINSEQ_1:def 4;

      end;

      :: original: Im

      redefine

      func Im S -> FinSequence of REAL ;

      coherence

      proof

        ( rng ( Im S)) c= REAL ;

        hence thesis by FINSEQ_1:def 4;

      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;

      :: INTEGR16:def1

      mode middle_volume of f,D -> FinSequence of COMPLEX means

      : Def1: ( len it ) = ( len D) & for i be Nat st i in ( dom D) holds ex c be Element of COMPLEX st c in ( rng (f | ( divset (D,i)))) & (it . i) = (c * ( vol ( divset (D,i))));

      correctness

      proof

        defpred P1[ Nat, set] means ex c be 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 be Nat st k in ( Seg ( len D)) holds ex x be Element of COMPLEX st P1[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( len D));

          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 ( rng (f | ( divset (D,k)))) is non empty by RELAT_1: 42;

          then

          consider c be object such that

           A4: c in ( rng (f | ( divset (D,k))));

          reconsider c as Element of COMPLEX by A4;

          (c * ( vol ( divset (D,k)))) is Element of COMPLEX by XCMPLX_0:def 2;

          hence thesis by A4;

        end;

        consider p be FinSequence of COMPLEX such that

         A5: ( dom p) = ( Seg ( len D)) & for k be Nat st k in ( Seg ( len D)) holds P1[k, (p . k)] from FINSEQ_1:sch 5( A2);

        ( len p) = ( len D) by A5, FINSEQ_1:def 3;

        hence thesis by A5, A1;

      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;

      let F be middle_volume of f, D;

      :: INTEGR16:def2

      func middle_sum (f,F) -> Element of COMPLEX equals ( Sum F);

      coherence ;

    end

    definition

      let A be non empty closed_interval Subset of REAL , f be Function of A, COMPLEX , T be DivSequence of A;

      :: INTEGR16:def3

      mode middle_volume_Sequence of f,T -> sequence of ( COMPLEX * ) means

      : Def3: for k be Element of NAT holds (it . k) is middle_volume of f, (T . k);

      correctness

      proof

        defpred P[ Element of NAT , set] means $2 is middle_volume of f, (T . $1);

        

         A1: for x be Element of NAT holds ex y be Element of ( COMPLEX * ) st P[x, y]

        proof

          let x be Element of NAT ;

          set y = the middle_volume of f, (T . x);

          reconsider y as Element of ( COMPLEX * ) by FINSEQ_1:def 11;

          y is middle_volume of f, (T . x);

          hence thesis;

        end;

        ex f be sequence of ( COMPLEX * ) st for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        hence thesis;

      end;

    end

    definition

      let A be non empty closed_interval Subset of REAL , f be Function of A, COMPLEX , T be DivSequence of A, S be middle_volume_Sequence of f, T, k be Element of NAT ;

      :: original: .

      redefine

      func S . k -> middle_volume of f, (T . k) ;

      coherence by Def3;

    end

    definition

      let A be non empty closed_interval Subset of REAL , f be Function of A, COMPLEX , T be DivSequence of A, S be middle_volume_Sequence of f, T;

      :: INTEGR16:def4

      func middle_sum (f,S) -> Complex_Sequence means

      : Def4: for i be Element of NAT holds (it . i) = ( middle_sum (f,(S . i)));

      existence

      proof

        deffunc H1( Element of NAT ) = ( middle_sum (f,(S . $1)));

        thus ex IT be Complex_Sequence st for i be Element of NAT holds (IT . i) = H1(i) from FUNCT_2:sch 4;

      end;

      uniqueness

      proof

        let F1,F2 be Complex_Sequence;

        assume that

         A1: for i be Element of NAT holds (F1 . i) = ( middle_sum (f,(S . i))) and

         A2: for i be Element of NAT holds (F2 . i) = ( middle_sum (f,(S . i)));

        for i be Element of NAT holds (F1 . i) = (F2 . i)

        proof

          let i be Element of NAT ;

          (F1 . i) = ( middle_sum (f,(S . i))) by A1

          .= (F2 . i) by A2;

          hence (F1 . i) = (F2 . i);

        end;

        hence F1 = F2 by FUNCT_2: 63;

      end;

    end

    begin

    theorem :: INTEGR16:2

    for f be PartFunc of REAL , COMPLEX , A be Subset of REAL holds ( Re (f | A)) = (( Re f) | A)

    proof

      let f be PartFunc of REAL , COMPLEX , A be Subset of REAL ;

       A1:

      now

        let c be object;

        assume

         A2: c in ( dom (( Re f) | A));

        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;

      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 thesis by A1, FUNCT_1: 2;

    end;

    theorem :: INTEGR16:3

    for f be PartFunc of REAL , COMPLEX , A be Subset of REAL holds ( Im (f | A)) = (( Im f) | A)

    proof

      let f be PartFunc of REAL , COMPLEX , A be Subset of REAL ;

       A1:

      now

        let c be object;

        assume

         A2: c in ( dom (( Im f) | A));

        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;

      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 thesis by A1, FUNCT_1: 2;

    end;

    registration

      let A be non empty closed_interval Subset of REAL ;

      let f be Function of A, COMPLEX ;

      cluster ( Re f) -> quasi_total;

      correctness

      proof

        ( dom f) = A by FUNCT_2:def 1;

        then ( dom ( Re f)) = A by COMSEQ_3:def 3;

        hence thesis by FUNCT_2:def 1;

      end;

      cluster ( Im f) -> quasi_total;

      correctness

      proof

        ( dom f) = A by FUNCT_2:def 1;

        then ( dom ( Im f)) = A by COMSEQ_3:def 4;

        hence thesis by FUNCT_2:def 1;

      end;

    end

    theorem :: INTEGR16:4

    

     Th4: for A be non empty closed_interval Subset of REAL , f be Function of A, COMPLEX , D be Division of A, S be 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 , f be Function of A, COMPLEX , D be Division of A, S be middle_volume of 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 RS) = ( len D) by A1, FINSEQ_1:def 3;

      for i be Nat st i in ( dom D) holds ex r be Element of REAL st r in ( rng (( Re f) | ( divset (D,i)))) & (RS . i) = (r * ( vol ( divset (D,i))))

      proof

        let i be Nat such that

         A4: i in ( dom D);

        consider c be 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 r;

        consider t be object 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;

        r = ( 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 r in ( rng (( Re f) | ( divset (D,i)))) by A7, A10, FUNCT_1:def 3;

        

        thus (RS . i) = ( Re (S . i)) by A6, COMSEQ_3:def 3

        .= (r * ( vol ( divset (D,i)))) by A5, Th1;

      end;

      hence ( Re S) is middle_volume of ( Re f), D by A3, INTEGR15:def 1;

      

       A11: ( dom S) = ( dom ( Im S)) by COMSEQ_3:def 4;

      set IS = ( Im S);

      

       A12: ( len IS) = ( len D) by A2, A11, FINSEQ_1:def 3;

      for i be Nat st i in ( dom D) holds ex r be Element of REAL st r in ( rng (( Im f) | ( divset (D,i)))) & (IS . i) = (r * ( vol ( divset (D,i))))

      proof

        let i be Nat such that

         A13: i in ( dom D);

        consider c be 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 r;

        consider t be object 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;

        r = ( 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 r in ( rng (( Im f) | ( divset (D,i)))) by A16, A19, FUNCT_1:def 3;

        

        thus (IS . i) = ( Im (S . i)) by A15, COMSEQ_3:def 4

        .= (r * ( vol ( divset (D,i)))) by A14, Th1;

      end;

      hence ( Im S) is middle_volume of ( Im f), D by A12, INTEGR15:def 1;

    end;

    

     Lm2: ( Sum ( <*> COMPLEX )) = 0 by BINOP_2: 1, FINSOP_1: 10;

    

     Lm3: for F be FinSequence of COMPLEX , x be Element of COMPLEX holds ( Sum (F ^ <*x*>)) = (( Sum F) + x)

    proof

      let F be FinSequence of COMPLEX , x be Element of COMPLEX ;

      

      thus ( Sum (F ^ <*x*>)) = ( addcomplex . (( addcomplex $$ F),x)) by FINSOP_1: 4

      .= (( Sum F) + x) by BINOP_2:def 3;

    end;

    theorem :: INTEGR16:5

    

     Th5: for F be FinSequence of COMPLEX , x be Element of COMPLEX holds ( Re (F ^ <*x*>)) = (( Re F) ^ <*( Re x)*>)

    proof

      let F be FinSequence of COMPLEX , x be Element of COMPLEX ;

      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 F1) = ( 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 F2) by FINSEQ_1:def 7;

      now

        let k be Nat;

        assume

         A5: k in ( dom F1);

        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

          per cases ;

            suppose

             A8: k = (( len F) + 1);

            

            thus (F1 . k) = ( Re ((F ^ <*x*>) . k)) by A5, COMSEQ_3:def 3

            .= ( Re x) by A8, FINSEQ_1: 42

            .= (F2 . (( len ( Re F)) + 1)) by FINSEQ_1: 42

            .= (F2 . k) by A8, A1, A2, FINSEQ_1:def 3;

          end;

            suppose

             A9: k <> (( len F) + 1);

            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));

            then

             A10: k in ( dom F) by FINSEQ_1:def 3;

            then

             A11: k in ( dom ( Re F)) by COMSEQ_3:def 3;

            

            thus (F1 . 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

            .= (F2 . k) by A11, FINSEQ_1:def 7;

          end;

        end;

        hence (F1 . k) = (F2 . k);

      end;

      hence ( Re (F ^ <*x*>)) = (( Re F) ^ <*( Re x)*>) by A4, FINSEQ_1: 13;

    end;

    theorem :: INTEGR16:6

    

     Th6: for F be FinSequence of COMPLEX , x be Element of COMPLEX holds ( Im (F ^ <*x*>)) = (( Im F) ^ <*( Im x)*>)

    proof

      let F be FinSequence of COMPLEX , x be Element of COMPLEX ;

      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 F1) = ( 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 F2) by FINSEQ_1:def 7;

      now

        let k be Nat;

        assume

         A5: k in ( dom F1);

        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

          per cases ;

            suppose

             A8: k = (( len F) + 1);

            

            thus (F1 . k) = ( Im ((F ^ <*x*>) . k)) by A5, COMSEQ_3:def 4

            .= ( Im x) by A8, FINSEQ_1: 42

            .= (F2 . (( len ( Im F)) + 1)) by FINSEQ_1: 42

            .= (F2 . k) by A8, A1, A2, FINSEQ_1:def 3;

          end;

            suppose

             A9: k <> (( len F) + 1);

            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));

            then

             A10: k in ( dom F) by FINSEQ_1:def 3;

            then

             A11: k in ( dom ( Im F)) by COMSEQ_3:def 4;

            

            thus (F1 . 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

            .= (F2 . k) by A11, FINSEQ_1:def 7;

          end;

        end;

        hence (F1 . k) = (F2 . k);

      end;

      hence ( Im (F ^ <*x*>)) = (( Im F) ^ <*( Im x)*>) by A4, FINSEQ_1: 13;

    end;

    theorem :: INTEGR16:7

    

     Th7: for F be FinSequence of COMPLEX , Fr be FinSequence of REAL st Fr = ( Re F) holds ( Sum Fr) = ( Re ( Sum F))

    proof

      defpred P[ Nat] means for F be FinSequence of COMPLEX , Fr be FinSequence of REAL st ( len F) = $1 & Fr = ( Re F) holds ( Sum Fr) = ( Re ( Sum F));

      

       A1: P[ 0 ]

      proof

        let F be FinSequence of COMPLEX , Fr be FinSequence of REAL ;

        assume

         A2: ( len F) = 0 & Fr = ( Re 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;

      end;

       A4:

      now

        let k be Nat;

        assume

         A5: P[k];

        now

          let F be FinSequence of COMPLEX , Fr be FinSequence of REAL ;

          assume

           A6: ( len F) = (k + 1) & Fr = ( Re F);

          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;

        end;

        hence P[(k + 1)];

      end;

      

       A9: for k be Nat holds P[k] from NAT_1:sch 2( A1, A4);

      let F be FinSequence of COMPLEX , Fr be FinSequence of REAL ;

      assume

       A10: Fr = ( Re F);

      ( len F) is Element of NAT ;

      hence ( Sum Fr) = ( Re ( Sum F)) by A9, A10;

    end;

    theorem :: INTEGR16:8

    

     Th8: for F be FinSequence of COMPLEX , Fi be FinSequence of REAL st Fi = ( Im F) holds ( Sum Fi) = ( Im ( Sum F))

    proof

      defpred P[ Nat] means for F be FinSequence of COMPLEX , Fi be FinSequence of REAL st ( len F) = $1 & Fi = ( Im F) holds ( Sum Fi) = ( Im ( Sum F));

      

       A1: P[ 0 ]

      proof

        let F be FinSequence of COMPLEX , Fi be FinSequence of REAL ;

        assume

         A2: ( len F) = 0 & Fi = ( Im 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;

      end;

       A4:

      now

        let k be Nat;

        assume

         A5: P[k];

        now

          let F be FinSequence of COMPLEX , Fi be FinSequence of REAL ;

          assume

           A6: ( len F) = (k + 1) & Fi = ( Im F);

          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;

        end;

        hence P[(k + 1)];

      end;

      

       A9: for k be Nat holds P[k] from NAT_1:sch 2( A1, A4);

      let F be FinSequence of COMPLEX , Fi be FinSequence of REAL ;

      assume

       A10: Fi = ( Im F);

      ( len F) is Element of NAT ;

      hence ( Sum Fi) = ( Im ( Sum F)) by A9, A10;

    end;

    theorem :: INTEGR16:9

    for A be non empty closed_interval Subset of REAL , f be Function of A, COMPLEX , D be Division of A, F be middle_volume of f, D, Fr be 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 be non empty closed_interval Subset of REAL , f be Function of A, COMPLEX , D be Division of A, F be middle_volume of f, D, Fi be 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 ;

      :: INTEGR16:def5

      attr f is integrable means ( Re f) is integrable & ( Im f) is integrable;

    end

    theorem :: INTEGR16:11

    

     Th11: for f be 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 ;

      thus f is bounded implies (( Re f) is bounded & ( Im f) is bounded)

      proof

        assume f is bounded;

        then

        consider r be Real such that

         A1: for y be set st y in ( dom f) holds |.(f . y).| < r by COMSEQ_2:def 3;

        now

          let y be set;

          assume

           A2: y in ( dom ( Re f));

          then

           A3: y in ( dom f) by COMSEQ_3:def 3;

           |.( Re (f . y)).| <= |.(f . y).| by COMPLEX1: 79;

          then |.( Re (f . y)).| < r by A1, A3, XXREAL_0: 2;

          hence |.(( Re f) . y).| < r by A2, COMSEQ_3:def 3;

        end;

        hence ( Re f) is bounded by COMSEQ_2:def 3;

        now

          let y be set;

          assume

           A4: y in ( dom ( Im f));

          then

           A5: y in ( dom f) by COMSEQ_3:def 4;

           |.( Im (f . y)).| <= |.(f . y).| by COMPLEX1: 79;

          then |.( Im (f . y)).| < r by A1, A5, XXREAL_0: 2;

          hence |.(( Im f) . y).| < r by A4, COMSEQ_3:def 4;

        end;

        hence ( Im f) is bounded by COMSEQ_2:def 3;

      end;

      thus (( Re f) is bounded & ( Im f) is bounded) implies f is bounded

      proof

        assume

         A6: ( Re f) is bounded & ( Im f) is bounded;

        then

        consider r1 be Real such that

         A7: for y be set st y in ( dom ( Re f)) holds |.(( Re f) . y).| < r1 by COMSEQ_2:def 3;

        consider r2 be Real such that

         A8: for y be set st y in ( dom ( Im f)) holds |.(( Im f) . y).| < r2 by A6, COMSEQ_2:def 3;

        now

          let y be set;

          assume

           A9: y in ( dom f);

          then

           A10: y in ( dom ( Re f)) by COMSEQ_3:def 3;

          then |.(( Re f) . y).| < r1 by A7;

          then

           A11: |.( Re (f . y)).| < r1 by A10, COMSEQ_3:def 3;

          

           A12: y in ( dom ( Im f)) by A9, COMSEQ_3:def 4;

          then |.(( Im f) . y).| < r2 by A8;

          then

           A13: |.( Im (f . y)).| < r2 by A12, COMSEQ_3:def 4;

          

           A14: |.(f . y).| <= ( |.( Re (f . y)).| + |.( Im (f . y)).|) by COMPLEX1: 78;

          ( |.( Re (f . y)).| + |.( Im (f . y)).|) < (r1 + r2) by A11, A13, XREAL_1: 8;

          hence |.(f . y).| < (r1 + r2) by A14, XXREAL_0: 2;

        end;

        hence f is bounded by COMSEQ_2:def 3;

      end;

    end;

    theorem :: INTEGR16:12

    for A be non empty Subset of REAL , f be PartFunc of REAL , COMPLEX , g be Function of A, COMPLEX st f = g holds ( Re f) = ( Re g) & ( Im f) = ( Im g);

    theorem :: INTEGR16:13

    

     Th13: for A be non empty closed_interval Subset of REAL , f be 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 , f be Function of A, COMPLEX ;

      ( 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 thesis;

    end;

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be Function of A, COMPLEX ;

      :: INTEGR16:def6

      func integral (f) -> Element of COMPLEX equals (( integral ( Re f)) + (( integral ( Im f)) * <i> ));

      correctness by XCMPLX_0:def 2;

    end

    theorem :: INTEGR16:14

    

     Th14: for A be non empty closed_interval Subset of REAL , f be Function of A, COMPLEX , T be DivSequence of A, S be 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 , f be Function of A, COMPLEX , T be DivSequence of A, S be middle_volume_Sequence of f, T;

      assume that

       A1: f is bounded & f is integrable and

       A2: ( delta T) is convergent & ( lim ( delta T)) = 0 ;

      set seq = ( middle_sum (f,S));

      set xs = ( integral f);

      

       A3: ( Re f) is bounded & ( Re f) is integrable by A1, Th13;

      

       A4: ( Im f) is bounded & ( Im f) is integrable by A1, Th13;

      reconsider xseq = seq as sequence of COMPLEX ;

      ex rseqi be Real_Sequence st for k be Nat holds (rseqi . k) = ( Re (xseq . k)) & rseqi is convergent & ( Re xs) = ( lim rseqi)

      proof

        reconsider pjinf = ( Re f) as Function of A, REAL ;

        defpred P[ Element of NAT , set] means $2 = ( Re (S . $1));

        

         A5: for x be Element of NAT holds ex y be Element of ( REAL * ) st P[x, y]

        proof

          let x be Element of NAT ;

          ( Re (S . x)) is Element of ( REAL * ) by FINSEQ_1:def 11;

          hence thesis;

        end;

        consider F be sequence of ( REAL * ) such that

         A6: for x be Element of NAT holds P[x, (F . x)] from FUNCT_2:sch 3( A5);

        

         A7: for x be Element of NAT holds ( dom ( Re (S . x))) = ( Seg ( len (S . x)))

        proof

          let x be Element of NAT ;

          

          thus ( dom ( Re (S . x))) = ( dom (S . x)) by COMSEQ_3:def 3

          .= ( Seg ( len (S . x))) by FINSEQ_1:def 3;

        end;

        for k be Element of NAT holds (F . k) is middle_volume of pjinf, (T . k)

        proof

          let k be Element of NAT ;

          set Tk = (T . k);

          reconsider Fk = (F . k) as FinSequence of REAL ;

          

           A8: (F . k) = ( Re (S . k)) by A6;

          

          then

           A9: ( dom Fk) = ( Seg ( len (S . k))) by A7

          .= ( Seg ( len Tk)) by Def1;

          then

           A10: ( dom Fk) = ( dom Tk) by FINSEQ_1:def 3;

           A11:

          now

            let j be Nat;

            assume

             A12: j in ( dom Tk);

            then

            consider r be 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;

            consider t be object 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;

            

            thus (Fk . j) = ( Re ((S . k) . j)) by A8, A10, A12, COMSEQ_3:def 3

            .= (v * ( vol ( divset ((T . k),j)))) by A14, Th1;

          end;

          ( len Fk) = ( len Tk) by A9, FINSEQ_1:def 3;

          hence thesis by A11, INTEGR15:def 1;

        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 be Nat holds (rseqi . k) = ( Re (xseq . k))

        proof

          let k be Nat;

          reconsider kk = k as Element of NAT by ORDINAL1:def 12;

          

           A20: ( Re (S . kk)) is middle_volume of ( Re f), (T . kk) by Th4;

          

          thus (rseqi . k) = ( middle_sum (pjinf,(pjis . kk))) by INTEGR15:def 4

          .= ( Re ( middle_sum (f,(S . kk)))) by A6, A20, Th7

          .= ( Re (xseq . k)) by Def4;

        end;

        take rseqi;

        ( lim ( middle_sum (pjinf,pjis))) = ( integral pjinf) by A2, A3, INTEGR15: 9;

        hence thesis by A2, A3, A19, COMPLEX1: 12, INTEGR15: 9;

      end;

      then

      consider rseqi be Real_Sequence such that

       A21: for k be Nat holds (rseqi . k) = ( Re (xseq . k)) & rseqi is convergent & ( Re xs) = ( lim rseqi);

      ex iseqi be Real_Sequence st for k be Nat holds (iseqi . k) = ( Im (xseq . k)) & iseqi is convergent & ( Im xs) = ( lim iseqi)

      proof

        reconsider pjinf = ( Im f) as Function of A, REAL ;

        defpred P[ Element of NAT , set] means $2 = ( Im (S . $1));

        

         A22: for x be Element of NAT holds ex y be Element of ( REAL * ) st P[x, y]

        proof

          let x be Element of NAT ;

          ( Im (S . x)) is Element of ( REAL * ) by FINSEQ_1:def 11;

          hence thesis;

        end;

        consider F be sequence of ( REAL * ) such that

         A23: for x be Element of NAT holds P[x, (F . x)] from FUNCT_2:sch 3( A22);

        

         A24: for x be Element of NAT holds ( dom ( Im (S . x))) = ( Seg ( len (S . x)))

        proof

          let x be Element of NAT ;

          ( dom ( Im (S . x))) = ( dom (S . x)) by COMSEQ_3:def 4

          .= ( Seg ( len (S . x))) by FINSEQ_1:def 3;

          hence thesis;

        end;

        for k be Element of NAT holds (F . k) is middle_volume of pjinf, (T . k)

        proof

          let k be Element of NAT ;

          reconsider Tk = (T . k) as FinSequence;

          reconsider Fk = (F . k) as FinSequence of REAL ;

          

           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

            let j be Nat;

            assume

             A29: j in ( dom Tk);

            then

            consider r be 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;

            consider t be object 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;

            

            thus (Fk . j) = ( Im ((S . k) . j)) by A25, A27, A29, COMSEQ_3:def 4

            .= (v * ( vol ( divset ((T . k),j)))) by A31, Th1;

          end;

          ( len Fk) = ( len Tk) by A26, FINSEQ_1:def 3;

          hence thesis by A28, INTEGR15:def 1;

        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 be Nat holds (iseqi . k) = ( Im (xseq . k))

        proof

          let k be Nat;

          reconsider kk = k as Element of NAT by ORDINAL1:def 12;

          

           A37: ( Im (S . kk)) is middle_volume of ( Im f), (T . kk) by Th4;

          

          thus (iseqi . k) = ( middle_sum (pjinf,(pjis . kk))) by INTEGR15:def 4

          .= ( Im ( middle_sum (f,(S . kk)))) by A23, A37, Th8

          .= ( Im (xseq . k)) by Def4;

        end;

        take iseqi;

        ( lim ( middle_sum (pjinf,pjis))) = ( integral pjinf) by A2, A4, INTEGR15: 9;

        hence thesis by A2, A4, A36, COMPLEX1: 12, INTEGR15: 9;

      end;

      then

      consider iseqi be Real_Sequence such that

       A38: for k be Nat holds (iseqi . k) = ( Im (xseq . k)) & iseqi is convergent & ( Im xs) = ( lim iseqi);

      thus ( middle_sum (f,S)) is convergent by A21, A38, COMSEQ_3: 38;

      

      thus ( lim ( middle_sum (f,S))) = (( lim rseqi) + (( lim iseqi) * <i> )) by A21, A38, COMSEQ_3: 39

      .= ( integral f) by A21, A38, COMPLEX1: 13;

    end;

    theorem :: INTEGR16:15

    for A be non empty closed_interval Subset of REAL , f be Function of A, COMPLEX st f is bounded holds f is integrable iff ex I be Element of COMPLEX st for T be DivSequence of A, S be 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 , f be Function of A, COMPLEX ;

      assume

       A1: f is bounded;

      hereby

        reconsider I = ( integral f) as Element of COMPLEX ;

        assume

         A2: f is integrable;

        take I;

        thus for T be DivSequence of A, S be 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;

      end;

      now

        assume ex I be Element of COMPLEX st for T be DivSequence of A, S be 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;

        then

        consider I be Element of COMPLEX such that

         A3: for T be DivSequence of A, S be 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

          set x = I;

          let T be DivSequence of A, Si be middle_volume_Sequence of ( Re f), T;

          defpred P[ Element of NAT , set] means ex H be FinSequence, z be FinSequence st H = (T . $1) & z = $2 & ( len z) = ( len H) & for j be Element of NAT st j in ( dom H) holds ex rji be Element of COMPLEX , tji be 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 = x as Element of COMPLEX ;

          

           A5: for k be Element of NAT holds ex y be Element of ( COMPLEX * ) st P[k, y]

          proof

            let k be Element of NAT ;

            reconsider Tk = (T . k) as FinSequence;

            defpred P1[ Nat, set] means ex j be Element of NAT st $1 = j & ex rji be Element of COMPLEX , tji be 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 be Nat st j in ( Seg ( len Tk)) holds ex x be Element of COMPLEX st P1[j, x]

            proof

              let j0 be Nat;

              assume

               A7: j0 in ( Seg ( len Tk));

              then

              reconsider j = j0 as Element of NAT ;

              j in ( dom Tk) by A7, FINSEQ_1:def 3;

              then

              consider r be 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 be object 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 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 by XCMPLX_0:def 2;

              take x;

              thus P1[j0, x] by A9, A10, A11, A12;

            end;

            consider p be FinSequence of COMPLEX such that

             A13: ( dom p) = ( Seg ( len Tk)) & for j be Nat st j in ( Seg ( len Tk)) holds P1[j, (p . j)] from FINSEQ_1:sch 5( A6);

            reconsider x = p as Element of ( COMPLEX * ) by FINSEQ_1:def 11;

            take x;

             A14:

            now

              let jj0 be Element of NAT ;

              reconsider j0 = jj0 as Nat;

              

               A15: ( dom Tk) = ( Seg ( len Tk)) by FINSEQ_1:def 3;

              assume jj0 in ( dom Tk);

              then P1[j0, (p . j0)] by A13, A15;

              hence ex rji be Element of COMPLEX , tji be 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);

            end;

            ( len p) = ( len Tk) by A13, FINSEQ_1:def 3;

            hence P[k, x] by A14;

          end;

          consider S be sequence of ( COMPLEX * ) such that

           A16: for x be Element of NAT holds P[x, (S . x)] from FUNCT_2:sch 3( A5);

          for k be Element of NAT holds (S . k) is middle_volume of f, (T . k)

          proof

            let k be Element of NAT ;

            consider H be FinSequence, z be FinSequence such that

             A17: H = (T . k) & z = (S . k) & ( len H) = ( len z) and

             A18: for j be Element of NAT st j in ( dom H) holds ex rji be Element of COMPLEX , tji be 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

              let x be Nat;

              assume

               A20: x in ( dom H);

              then

              reconsider j = x as Element of NAT ;

              consider rji be Element of COMPLEX , tji be 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;

              thus rji in ( rng (f | ( divset ((T . k),x)))) by A21, A22, FUNCT_1: 3;

              thus (z . x) = (rji * ( vol ( divset ((T . k),x)))) by A23;

            end;

            thus thesis by A17, A19, Def1;

          end;

          then

          reconsider S as middle_volume_Sequence of f, T by Def3;

          set seq = ( middle_sum (f,S));

          reconsider xseq = seq as sequence of COMPLEX ;

          assume ( delta T) is convergent & ( lim ( delta T)) = 0 ;

          then

           A24: seq is convergent & ( lim seq) = x by A3;

          reconsider rseqi = ( Re seq) as Real_Sequence;

          

           A25: for k be 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 be Element of NAT holds (rseqi . k) = (( middle_sum (( Re f),Si)) . k)

          proof

            let k be Element of NAT ;

            consider H be FinSequence, z be FinSequence such that

             A26: H = (T . k) and

             A27: z = (S . k) and

             A28: ( len H) = ( len z) and

             A29: for j be Element of NAT st j in ( dom H) holds ex rji be Element of COMPLEX , tji be 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 be Nat st j in ( dom ( Re (S . k))) holds (( Re (S . k)) . j) = ((Si . k) . j)

            proof

              let j0 be Nat;

              reconsider j = j0 as Element of NAT by ORDINAL1:def 12;

              assume

               A32: j0 in ( dom ( Re (S . k)));

              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 be Element of COMPLEX , tji be 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 thesis;

            end;

            

             A40: for j0 be object 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;

          end;

          hence ( middle_sum (( Re f),Si)) is convergent & ( lim ( middle_sum (( Re f),Si))) = Ii by A25, FUNCT_2: 63;

        end;

        ( Re f) is bounded by A1, Th13;

        then

         A41: ( Re f) is integrable by A4, INTEGR15: 10;

         A42:

        now

          set x = I;

          let T be DivSequence of A, Si be middle_volume_Sequence of ( Im f), T;

          defpred P[ Element of NAT , set] means ex H be FinSequence, z be FinSequence st H = (T . $1) & z = $2 & ( len z) = ( len H) & for j be Element of NAT st j in ( dom H) holds ex rji be Element of COMPLEX , tji be 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 = x as Element of COMPLEX ;

          

           A43: for k be Element of NAT holds ex y be Element of ( COMPLEX * ) st P[k, y]

          proof

            let k be Element of NAT ;

            reconsider Tk = (T . k) as FinSequence;

            defpred P1[ Nat, set] means ex j be Element of NAT st $1 = j & ex rji be Element of COMPLEX , tji be 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 be Nat st j in ( Seg ( len Tk)) holds ex x be Element of COMPLEX st P1[j, x]

            proof

              let j0 be Nat;

              assume

               A45: j0 in ( Seg ( len Tk));

              then

              reconsider j = j0 as Element of NAT ;

              j in ( dom Tk) by A45, FINSEQ_1:def 3;

              then

              consider r be 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 be object 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 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 by XCMPLX_0:def 2;

              take x;

              thus P1[j0, x] by A47, A48, A49, A50;

            end;

            consider p be FinSequence of COMPLEX such that

             A51: ( dom p) = ( Seg ( len Tk)) & for j be Nat st j in ( Seg ( len Tk)) holds P1[j, (p . j)] from FINSEQ_1:sch 5( A44);

            reconsider x = p as Element of ( COMPLEX * ) by FINSEQ_1:def 11;

            take x;

             A52:

            now

              let jj0 be Element of NAT ;

              reconsider j0 = jj0 as Nat;

              

               A53: ( dom Tk) = ( Seg ( len Tk)) by FINSEQ_1:def 3;

              assume jj0 in ( dom Tk);

              then P1[j0, (p . j0)] by A51, A53;

              hence ex rji be Element of COMPLEX , tji be 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);

            end;

            ( len p) = ( len Tk) by A51, FINSEQ_1:def 3;

            hence P[k, x] by A52;

          end;

          consider S be sequence of ( COMPLEX * ) such that

           A54: for x be Element of NAT holds P[x, (S . x)] from FUNCT_2:sch 3( A43);

          for k be Element of NAT holds (S . k) is middle_volume of f, (T . k)

          proof

            let k be Element of NAT ;

            consider H be FinSequence, z be FinSequence such that

             A55: H = (T . k) & z = (S . k) & ( len H) = ( len z) and

             A56: for j be Element of NAT st j in ( dom H) holds ex rji be Element of COMPLEX , tji be 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

              let x be Nat;

              assume

               A58: x in ( dom H);

              then

              reconsider j = x as Element of NAT ;

              consider rji be Element of COMPLEX , tji be 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;

              thus rji in ( rng (f | ( divset ((T . k),x)))) by A59, A60, FUNCT_1: 3;

              thus (z . x) = (rji * ( vol ( divset ((T . k),x)))) by A61;

            end;

            thus thesis by A55, A57, Def1;

          end;

          then

          reconsider S as middle_volume_Sequence of f, T by Def3;

          set seq = ( middle_sum (f,S));

          reconsider xseq = seq as sequence of COMPLEX ;

          assume ( delta T) is convergent & ( lim ( delta T)) = 0 ;

          then

           A62: seq is convergent & ( lim seq) = x by A3;

          reconsider rseqi = ( Im seq) as Real_Sequence;

          

           A63: for k be 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 be Element of NAT holds (rseqi . k) = (( middle_sum (( Im f),Si)) . k)

          proof

            let k be Element of NAT ;

            consider H be FinSequence, z be FinSequence such that

             A64: H = (T . k) and

             A65: z = (S . k) and

             A66: ( len H) = ( len z) and

             A67: for j be Element of NAT st j in ( dom H) holds ex rji be Element of COMPLEX , tji be 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 be Nat st j in ( dom ( Im (S . k))) holds (( Im (S . k)) . j) = ((Si . k) . j)

            proof

              let j0 be Nat;

              reconsider j = j0 as Element of NAT by ORDINAL1:def 12;

              assume

               A70: j0 in ( dom ( Im (S . k)));

              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 be Element of COMPLEX , tji be 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 thesis;

            end;

            

             A78: for j0 be object 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;

          end;

          hence ( middle_sum (( Im f),Si)) is convergent & ( lim ( middle_sum (( Im f),Si))) = Ic by A63, FUNCT_2: 63;

        end;

        ( Im f) is bounded by A1, Th13;

        then ( Im f) is integrable by A42, INTEGR15: 10;

        hence f is integrable by A41;

      end;

      hence thesis;

    end;

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of REAL , COMPLEX ;

      :: INTEGR16:def7

      pred f is_integrable_on A means ( Re f) is_integrable_on A & ( Im f) is_integrable_on A;

    end

    definition

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of REAL , COMPLEX ;

      :: INTEGR16:def8

      func integral (f,A) -> Element of COMPLEX equals (( integral (( Re f),A)) + (( integral (( Im f),A)) * <i> ));

      correctness by XCMPLX_0:def 2;

    end

    

     Lm4: for f be PartFunc of REAL , COMPLEX , A be Subset of REAL holds ( Re (f | A)) = (( Re f) | A) & ( Im (f | A)) = (( Im f) | A)

    proof

      let f be PartFunc of REAL , COMPLEX , A be Subset of REAL ;

      ( 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

        let x be object;

        assume

         A2: x in ( dom (( Re f) | A));

        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;

      end;

      hence (( Re f) | A) = ( Re (f | A)) by A1, FUNCT_1: 2;

      ( 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

        let x be object;

        assume

         A7: x in ( dom (( Im f) | A));

        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;

      end;

      hence thesis by A6, FUNCT_1: 2;

    end;

    theorem :: INTEGR16:16

    for A be non empty closed_interval Subset of REAL , f be PartFunc of REAL , COMPLEX , g be 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 , f be PartFunc of REAL , COMPLEX , g be Function of A, COMPLEX ;

      assume

       A1: (f | A) = g;

      thus f is_integrable_on A implies g is integrable

      proof

        assume

         A2: f is_integrable_on A;

        ( 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;

          ( 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;

          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;

          ( Im g) = ( Im g0)

          .= G by A1, Lm4;

          hence ( Im g) is integrable by A5;

        end;

        hence thesis;

      end;

      assume

       A6: g is integrable;

      ( Re f) is_integrable_on A & ( Im f) is_integrable_on A by A1, Lm4, A6;

      hence thesis;

    end;

    theorem :: INTEGR16:17

    for A be non empty closed_interval Subset of REAL , f be PartFunc of REAL , COMPLEX , g be 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 , f be PartFunc of REAL , COMPLEX , g be Function of A, COMPLEX ;

      assume

       A1: (f | A) = 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;

    end;

    definition

      let a,b be Real;

      let f be PartFunc of REAL , COMPLEX ;

      :: INTEGR16:def9

      func integral (f,a,b) -> Element of COMPLEX equals (( integral (( Re f),a,b)) + (( integral (( Im f),a,b)) * <i> ));

      correctness by XCMPLX_0:def 2;

    end

    begin

    theorem :: INTEGR16:18

    

     Th18: for c be Complex, f be 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, f be PartFunc of REAL , COMPLEX ;

      

       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

        let x be object;

        assume

         A9: x in ( dom ( Re (c (#) f)));

        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;

      end;

      hence ( Re (c (#) f)) = ((( Re c) (#) ( Re f)) - (( Im c) (#) ( Im f))) by A7, FUNCT_1: 2;

      now

        let x be object;

        assume

         A11: x in ( dom ( Im (c (#) f)));

        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;

      end;

      hence ( Im (c (#) f)) = ((( Re c) (#) ( Im f)) + (( Im c) (#) ( Re f))) by A8, FUNCT_1: 2;

    end;

    theorem :: INTEGR16:19

    for A be non empty closed_interval Subset of REAL , f1,f2 be 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 ;

      let f1,f2 be PartFunc of REAL , COMPLEX ;

      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;

      

       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;

        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;

        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;

      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;

      (( 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 thesis;

      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)));

      ( 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)));

    end;

    theorem :: INTEGR16:20

    for r be Real holds for A be non empty closed_interval Subset of REAL holds for f be 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;

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of REAL , COMPLEX ;

      assume that

       A1: A c= ( dom f) and

       A2: f is_integrable_on A and

       A3: (f | A) is bounded;

      

       A4: ( Re f) is_integrable_on A & ( Im f) is_integrable_on A by A2;

      

       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;

        thus ( integral ((r (#) ( Im f)),A)) = (r * ( integral (( Im f),A))) by A4, A6, A7, INTEGRA6: 9;

      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 thesis by A5, MESFUN6C: 2;

      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;

        then (r (#) ( Re f)) is_integrable_on A & (r (#) ( Im f)) is_integrable_on A by A9, A10, INTEGRA6: 9;

        hence thesis by MESFUN6C: 2;

      end;

      hence (r (#) f) is_integrable_on 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 thesis;

    end;

    theorem :: INTEGR16:21

    for c be Complex, A be non empty closed_interval Subset of REAL , f be 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;

      let A be non empty closed_interval Subset of REAL ;

      let f be PartFunc of REAL , COMPLEX ;

      assume that

       A1: A c= ( dom f) and

       A2: f is_integrable_on A and

       A3: (f | A) is bounded;

      

       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;

        thus ( Im (c * ( integral (f,A)))) = ((( Re c) * ( integral (( Im f),A))) + (( Im c) * ( integral (( Re f),A)))) by A5, A6, COMPLEX1: 9;

      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;

      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;

      

       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 thesis by A15;

    end;

    theorem :: INTEGR16:22

    for f be PartFunc of REAL , COMPLEX , A be non empty closed_interval Subset of REAL , a,b be Real st A = [.a, b.] holds ( integral (f,A)) = ( integral (f,a,b))

    proof

      let f be PartFunc of REAL , COMPLEX , A be non empty closed_interval Subset of REAL , a,b be Real;

      assume

       A1: A = [.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));

    end;

    theorem :: INTEGR16:23

    for f be PartFunc of REAL , COMPLEX , A be non empty closed_interval Subset of REAL , a,b be Real st A = [.b, a.] holds ( - ( integral (f,A))) = ( integral (f,a,b))

    proof

      let f be PartFunc of REAL , COMPLEX , A be non empty closed_interval Subset of REAL , a,b be Real;

      assume

       A1: A = [.b, a.];

      

       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 thesis by A5;

    end;