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

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

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

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
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 object such that

A7: t in dom (f | (divset (D,i))) and

A8: c = (f | (divset (D,i))) . t by A5, FUNCT_1:def 3;

t in (dom f) /\ (divset (D,i)) by A7, RELAT_1:61;

then t in dom f by XBOOLE_0:def 4;

then A9: t in dom (Re f) by COMSEQ_3:def 3;

A10: dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) by RELAT_1:61

.= (dom (Re f)) /\ (divset (D,i)) by COMSEQ_3:def 3

.= dom ((Re f) | (divset (D,i))) by RELAT_1:61 ;

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;( 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 object such that

A7: t in dom (f | (divset (D,i))) and

A8: c = (f | (divset (D,i))) . t by A5, FUNCT_1:def 3;

t in (dom f) /\ (divset (D,i)) by A7, RELAT_1:61;

then t in dom f by XBOOLE_0:def 4;

then A9: t in dom (Re f) by COMSEQ_3:def 3;

A10: dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) by RELAT_1:61

.= (dom (Re f)) /\ (divset (D,i)) by COMSEQ_3:def 3

.= dom ((Re f) | (divset (D,i))) by RELAT_1:61 ;

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

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

hence
Im S is middle_volume of Im f,D
by A12, INTEGR15:def 1; :: thesis: verum
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 object such that

A16: t in dom (f | (divset (D,i))) and

A17: c = (f | (divset (D,i))) . t by A14, FUNCT_1:def 3;

t in (dom f) /\ (divset (D,i)) by A16, RELAT_1:61;

then t in dom f by XBOOLE_0:def 4;

then A18: t in dom (Im f) by COMSEQ_3:def 4;

A19: dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) by RELAT_1:61

.= (dom (Im f)) /\ (divset (D,i)) by COMSEQ_3:def 4

.= dom ((Im f) | (divset (D,i))) by RELAT_1:61 ;

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;( 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 object such that

A16: t in dom (f | (divset (D,i))) and

A17: c = (f | (divset (D,i))) . t by A14, FUNCT_1:def 3;

t in (dom f) /\ (divset (D,i)) by A16, RELAT_1:61;

then t in dom f by XBOOLE_0:def 4;

then A18: t in dom (Im f) by COMSEQ_3:def 4;

A19: dom (f | (divset (D,i))) = (dom f) /\ (divset (D,i)) by RELAT_1:61

.= (dom (Im f)) /\ (divset (D,i)) by COMSEQ_3:def 4

.= dom ((Im f) | (divset (D,i))) by RELAT_1:61 ;

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