let r be Real; for i being Nat
for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
let i be Nat; for A being non empty closed_interval Subset of REAL
for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
let A be non empty closed_interval Subset of REAL; for f being Function of A,REAL
for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
let f be Function of A,REAL; for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds
(lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
let D be Division of A; ( i in dom D & f | A is bounded_below & r >= 0 implies (lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) )
assume that
A1:
i in dom D
and
A2:
f | A is bounded_below
and
A3:
r >= 0
; (lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
dom (f | (divset (D,i))) =
(dom f) /\ (divset (D,i))
by RELAT_1:61
.=
A /\ (divset (D,i))
by FUNCT_2:def 1
.=
divset (D,i)
by A1, INTEGRA1:8, XBOOLE_1:28
;
then A4:
not rng (f | (divset (D,i))) is empty
by RELAT_1:42;
rng f is bounded_below
by A2, INTEGRA1:11;
then A5:
rng (f | (divset (D,i))) is bounded_below
by RELAT_1:70, XXREAL_2:44;
(lower_volume ((r (#) f),D)) . i =
(lower_bound (rng ((r (#) f) | (divset (D,i))))) * (vol (divset (D,i)))
by A1, INTEGRA1:def 7
.=
(lower_bound (rng (r (#) (f | (divset (D,i)))))) * (vol (divset (D,i)))
by RFUNCT_1:49
.=
(lower_bound (r ** (rng (f | (divset (D,i)))))) * (vol (divset (D,i)))
by Th18
.=
(r * (lower_bound (rng (f | (divset (D,i)))))) * (vol (divset (D,i)))
by A3, A4, A5, Th15
.=
r * ((lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))))
.=
r * ((lower_volume (f,D)) . i)
by A1, INTEGRA1:def 7
;
hence
(lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i)
; verum