let A be 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 )
let f be 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 D be 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 S be middle_volume of f,D; ( 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 Def5;
then A2:
dom S = Seg (len D)
by FINSEQ_1:def 3;
then P1:
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;
( 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 P20:
i in dom D
;
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 P21:
(
c in rng (f | (divset D,i)) &
S . i = c * (vol (divset D,i)) )
by P20, Def5;
P22:
i in dom (Re S)
by P20, A1, A2, FINSEQ_1:def 3;
set r =
Re c;
take
Re c
;
( Re c in rng ((Re f) | (divset D,i)) & (Re S) . i = (Re c) * (vol (divset D,i)) )
consider t being
set such that P23:
t in dom (f | (divset D,i))
and P24:
c = (f | (divset D,i)) . t
by P21, FUNCT_1:def 5;
t in (dom f) /\ (divset D,i)
by P23, RELAT_1:90;
then
t in dom f
by XBOOLE_0:def 4;
then P25:
t in dom (Re f)
by COMSEQ_3:def 3;
P26:
dom (f | (divset D,i)) =
(dom f) /\ (divset D,i)
by RELAT_1:90
.=
(dom (Re f)) /\ (divset D,i)
by COMSEQ_3:def 3
.=
dom ((Re f) | (divset D,i))
by RELAT_1:90
;
Re c =
Re (f . t)
by P23, P24, FUNCT_1:70
.=
(Re f) . t
by P25, COMSEQ_3:def 3
.=
((Re f) | (divset D,i)) . t
by P23, P26, FUNCT_1:70
;
hence
Re c in rng ((Re f) | (divset D,i))
by P23, P26, FUNCT_1:def 5;
(Re S) . i = (Re c) * (vol (divset D,i))
thus (Re S) . i =
Re (S . i)
by COMSEQ_3:def 3, P22
.=
(Re c) * (vol (divset D,i))
by P21, LM001
;
verum
end;
hence
Re S is middle_volume of Re f,D
by P1, INTEGR15:def 1; Im S is middle_volume of Im f,D
A3:
dom S = dom (Im S)
by COMSEQ_3:def 4;
set IS = Im S;
P2:
len (Im S) = len D
by A2, A3, 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;
( 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 P40:
i in dom D
;
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 P41:
(
c in rng (f | (divset D,i)) &
S . i = c * (vol (divset D,i)) )
by P40, Def5;
P42:
i in dom (Im S)
by P40, A2, A3, FINSEQ_1:def 3;
set r =
Im c;
take
Im c
;
( Im c in rng ((Im f) | (divset D,i)) & (Im S) . i = (Im c) * (vol (divset D,i)) )
consider t being
set such that P43:
t in dom (f | (divset D,i))
and P44:
c = (f | (divset D,i)) . t
by P41, FUNCT_1:def 5;
t in (dom f) /\ (divset D,i)
by P43, RELAT_1:90;
then
t in dom f
by XBOOLE_0:def 4;
then P45:
t in dom (Im f)
by COMSEQ_3:def 4;
P46:
dom (f | (divset D,i)) =
(dom f) /\ (divset D,i)
by RELAT_1:90
.=
(dom (Im f)) /\ (divset D,i)
by COMSEQ_3:def 4
.=
dom ((Im f) | (divset D,i))
by RELAT_1:90
;
Im c =
Im (f . t)
by P43, P44, FUNCT_1:70
.=
(Im f) . t
by P45, COMSEQ_3:def 4
.=
((Im f) | (divset D,i)) . t
by P43, P46, FUNCT_1:70
;
hence
Im c in rng ((Im f) | (divset D,i))
by P43, P46, FUNCT_1:def 5;
(Im S) . i = (Im c) * (vol (divset D,i))
thus (Im S) . i =
Im (S . i)
by COMSEQ_3:def 4, P42
.=
(Im c) * (vol (divset D,i))
by P41, LM001
;
verum
end;
hence
Im S is middle_volume of Im f,D
by P2, INTEGR15:def 1; verum