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

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

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