let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S
for r being Real st f is_measurable_on A & A c= dom f holds
r (#) f is_measurable_on A
let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL
for A being Element of S
for r being Real st f is_measurable_on A & A c= dom f holds
r (#) f is_measurable_on A
let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S
for r being Real st f is_measurable_on A & A c= dom f holds
r (#) f is_measurable_on A
let A be Element of S; :: thesis: for r being Real st f is_measurable_on A & A c= dom f holds
r (#) f is_measurable_on A
let r be Real; :: thesis: ( f is_measurable_on A & A c= dom f implies r (#) f is_measurable_on A )
assume that
A1: f is_measurable_on A and
A2: A c= dom f ; :: thesis: r (#) f is_measurable_on A
for r1 being real number holds A /\ (less_dom ((r (#) f),(R_EAL r1))) in S

proof

let r1 be real number ; :: thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S

now

per cases ( r <> 0 or r = 0 ) ;

suppose A5: r <> 0 ; :: thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S

A6: r1 in REAL by XREAL_0:def 1;
reconsider r0 = r1 / r as Real ;
A7: r1 = r * r0 by A5, XCMPLX_1:88;

now

per cases ( r > 0 or r < 0 ) by A5;

suppose A9: r > 0 ; :: thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S

for x being Element of X st x in less_dom (f,(R_EAL r0)) holds
x in less_dom ((r (#) f),(R_EAL r1))

proof

let x be Element of X; :: thesis: ( x in less_dom (f,(R_EAL r0)) implies x in less_dom ((r (#) f),(R_EAL r1)) )
assume A11: x in less_dom (f,(R_EAL r0)) ; :: thesis: x in less_dom ((r (#) f),(R_EAL r1))
then x in dom f by Def12;
then A13: x in dom (r (#) f) by Def6;
A14: f . x < R_EAL r0 by A11, Def12;
A15: r1 in REAL by XREAL_0:def 1;
then f . x < (R_EAL r1) / (R_EAL r) by A14, EXTREAL1:39;
then A17: (f . x) * (R_EAL r) < ((R_EAL r1) / (R_EAL r)) * (R_EAL r) by A9, XXREAL_3:83;
(R_EAL r1) / (R_EAL r) = r1 / r by A15, EXTREAL1:32;
then A19: ((R_EAL r1) / (R_EAL r)) * (R_EAL r) = (r1 / r) * r by EXTREAL1:13
.= r1 / (r / r) by XCMPLX_1:82
.= r1 / 1 by A5, XCMPLX_1:60
.= r1 ;
(r (#) f) . x = (R_EAL r) * (f . x) by A13, Def6;
hence x in less_dom ((r (#) f),(R_EAL r1)) by A13, A17, A19, Def12; :: thesis: verum

end;

then A21: less_dom (f,(R_EAL r0)) c= less_dom ((r (#) f),(R_EAL r1)) by SUBSET_1:7;
for x being Element of X st x in less_dom ((r (#) f),(R_EAL r1)) holds
x in less_dom (f,(R_EAL r0))

proof

let x be Element of X; :: thesis: ( x in less_dom ((r (#) f),(R_EAL r1)) implies x in less_dom (f,(R_EAL r0)) )
assume A23: x in less_dom ((r (#) f),(R_EAL r1)) ; :: thesis: x in less_dom (f,(R_EAL r0))
then A24: x in dom (r (#) f) by Def12;
(r (#) f) . x < R_EAL r1 by A23, Def12;
then (r (#) f) . x < (R_EAL r) * (R_EAL r0) by A7, EXTREAL1:38;
then A27: ((r (#) f) . x) / (R_EAL r) < ((R_EAL r) * (R_EAL r0)) / (R_EAL r) by A9, XXREAL_3:91;
(R_EAL r) * (R_EAL r0) = r * r0 by EXTREAL1:13;
then A29: ((R_EAL r) * (R_EAL r0)) / (R_EAL r) = (r * r0) / r by EXTREAL1:32
.= r0 / (r / r) by XCMPLX_1:78
.= r0 / 1 by A5, XCMPLX_1:60
.= r0 ;
( x in dom f & f . x = ((r (#) f) . x) / (R_EAL r) ) by A5, A24, Def6, Th6;
hence x in less_dom (f,(R_EAL r0)) by A27, A29, Def12; :: thesis: verum

end;

then less_dom ((r (#) f),(R_EAL r1)) c= less_dom (f,(R_EAL r0)) by SUBSET_1:7;
then less_dom (f,(R_EAL r0)) = less_dom ((r (#) f),(R_EAL r1)) by A21, XBOOLE_0:def 10;
hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S by A1, Def17; :: thesis: verum

end;

suppose A33: r < 0 ; :: thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S

for x being Element of X st x in great_dom (f,(R_EAL r0)) holds
x in less_dom ((r (#) f),(R_EAL r1))

proof

let x be Element of X; :: thesis: ( x in great_dom (f,(R_EAL r0)) implies x in less_dom ((r (#) f),(R_EAL r1)) )
assume A35: x in great_dom (f,(R_EAL r0)) ; :: thesis: x in less_dom ((r (#) f),(R_EAL r1))
then x in dom f by Def14;
then A37: x in dom (r (#) f) by Def6;
R_EAL r0 < f . x by A35, Def14;
then (R_EAL r1) / (R_EAL r) < f . x by A6, EXTREAL1:39;
then A40: (f . x) * (R_EAL r) < ((R_EAL r1) / (R_EAL r)) * (R_EAL r) by A33, XXREAL_3:114;
(R_EAL r1) / (R_EAL r) = r1 / r by A6, EXTREAL1:32;
then A42: ((R_EAL r1) / (R_EAL r)) * (R_EAL r) = (r1 / r) * r by EXTREAL1:13
.= r1 / (r / r) by XCMPLX_1:82
.= r1 / 1 by A5, XCMPLX_1:60
.= r1 ;
(r (#) f) . x = (R_EAL r) * (f . x) by A37, Def6;
hence x in less_dom ((r (#) f),(R_EAL r1)) by A37, A40, A42, Def12; :: thesis: verum

end;

then A44: great_dom (f,(R_EAL r0)) c= less_dom ((r (#) f),(R_EAL r1)) by SUBSET_1:7;
for x being Element of X st x in less_dom ((r (#) f),(R_EAL r1)) holds
x in great_dom (f,(R_EAL r0))

proof

let x be Element of X; :: thesis: ( x in less_dom ((r (#) f),(R_EAL r1)) implies x in great_dom (f,(R_EAL r0)) )
assume A46: x in less_dom ((r (#) f),(R_EAL r1)) ; :: thesis: x in great_dom (f,(R_EAL r0))
then A47: x in dom (r (#) f) by Def12;
(r (#) f) . x < R_EAL r1 by A46, Def12;
then (r (#) f) . x < (R_EAL r) * (R_EAL r0) by A7, EXTREAL1:38;
then A50: ((R_EAL r) * (R_EAL r0)) / (R_EAL r) < ((r (#) f) . x) / (R_EAL r) by A33, XXREAL_3:116;
(R_EAL r) * (R_EAL r0) = r * r0 by EXTREAL1:13;
then A52: ((R_EAL r) * (R_EAL r0)) / (R_EAL r) = (r * r0) / r by EXTREAL1:32
.= r0 / (r / r) by XCMPLX_1:78
.= r0 / 1 by A5, XCMPLX_1:60
.= r0 ;
( x in dom f & f . x = ((r (#) f) . x) / (R_EAL r) ) by A5, A47, Def6, Th6;
hence x in great_dom (f,(R_EAL r0)) by A50, A52, Def14; :: thesis: verum

end;

then less_dom ((r (#) f),(R_EAL r1)) c= great_dom (f,(R_EAL r0)) by SUBSET_1:7;
then great_dom (f,(R_EAL r0)) = less_dom ((r (#) f),(R_EAL r1)) by A44, XBOOLE_0:def 10;
hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S by A1, A2, Th33; :: thesis: verum

end;

end;

end;

hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S ; :: thesis: verum

end;

suppose A56: r = 0 ; :: thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S

now

per cases ( r1 > 0 or r1 <= 0 ) ;

suppose A58: r1 > 0 ; :: thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S

for x1 being set st x1 in A holds
x1 in A /\ (less_dom ((r (#) f),(R_EAL r1)))

proof

let x1 be set ; :: thesis: ( x1 in A implies x1 in A /\ (less_dom ((r (#) f),(R_EAL r1))) )
assume A60: x1 in A ; :: thesis: x1 in A /\ (less_dom ((r (#) f),(R_EAL r1)))
then reconsider x1 = x1 as Element of X ;
x1 in dom f by A2, A60;
then A62: x1 in dom (r (#) f) by Def6;
reconsider y = (r (#) f) . x1 as R_eal ;
y = (R_EAL r) * (f . x1) by A62, Def6
.= 0. by A56 ;
then x1 in less_dom ((r (#) f),(R_EAL r1)) by A58, A62, Def12;
hence x1 in A /\ (less_dom ((r (#) f),(R_EAL r1))) by A60, XBOOLE_0:def 4; :: thesis: verum

end;

then ( A /\ (less_dom ((r (#) f),(R_EAL r1))) c= A & A c= A /\ (less_dom ((r (#) f),(R_EAL r1))) ) by TARSKI:def 3, XBOOLE_1:17;
then A /\ (less_dom ((r (#) f),(R_EAL r1))) = A by XBOOLE_0:def 10;
hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S ; :: thesis: verum

end;

suppose A67: r1 <= 0 ; :: thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S

less_dom ((r (#) f),(R_EAL r1)) = {}

proof

assume less_dom ((r (#) f),(R_EAL r1)) <> {} ; :: thesis: contradiction
then consider x1 being Element of X such that
A70: x1 in less_dom ((r (#) f),(R_EAL r1)) by SUBSET_1:10;
A71: x1 in dom (r (#) f) by A70, Def12;
A72: (r (#) f) . x1 < R_EAL r1 by A70, Def12;
A73: (r (#) f) . x1 in rng (r (#) f) by A71, FUNCT_1:def 5;
for y being R_eal st y in rng (r (#) f) holds
not y < R_EAL r1

proof

let y be R_eal; :: thesis: ( y in rng (r (#) f) implies not y < R_EAL r1 )
assume y in rng (r (#) f) ; :: thesis: not y < R_EAL r1
then consider x being Element of X such that
A76: ( x in dom (r (#) f) & y = (r (#) f) . x ) by PARTFUN1:26;
y = (R_EAL r) * (f . x) by A76, Def6
.= 0. by A56 ;
hence not y < R_EAL r1 by A67; :: thesis: verum

end;

hence contradiction by A72, A73; :: thesis: verum

end;

hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S by PROB_1:10; :: thesis: verum

end;

end;

end;

hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S ; :: thesis: verum

end;

end;

end;

hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S ; :: thesis: verum

end;

hence r (#) f is_measurable_on A by Def17; :: thesis: verum