:: 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)) * <i>);
correctness
coherence
(integral (Re f)) + ((integral (Im f)) * <i>) 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)) * <i>);

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) * <i>) 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)) * <i>);
correctness
coherence
(integral ((Re f),A)) + ((integral ((Im f),A)) * <i>) 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)) * <i>);

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)) * <i>);
correctness
coherence
(integral ((Re f),a,b)) + ((integral ((Im f),a,b)) * <i>) 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)) * <i>);

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;