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 ;
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 ;
A6: i in dom (Re S) by ;
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 ;
t in (dom f) /\ (divset (D,i)) by ;
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
.= (Re f) . t by
.= ((Re f) | (divset (D,i))) . t by ;
hence Re c in rng ((Re f) | (divset (D,i))) by ; :: thesis: (Re S) . i = (Re c) * (vol (divset (D,i)))
thus (Re S) . i = Re (S . i) by
.= (Re c) * (vol (divset (D,i))) by ; :: thesis: verum
end;
hence Re S is middle_volume of Re f,D by ; :: 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 ;
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 ;
A15: i in dom (Im S) by ;
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 ;
t in (dom f) /\ (divset (D,i)) by ;
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
.= (Im f) . t by
.= ((Im f) | (divset (D,i))) . t by ;
hence Im c in rng ((Im f) | (divset (D,i))) by ; :: thesis: (Im S) . i = (Im c) * (vol (divset (D,i)))
thus (Im S) . i = Im (S . i) by
.= (Im c) * (vol (divset (D,i))) by ; :: thesis: verum
end;
hence Im S is middle_volume of Im f,D by ; :: thesis: verum