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 A3: r <> 0 ; :: thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S

A4: r1 in REAL by XREAL_0:def 1;
reconsider r0 = r1 / r as Real ;
A5: r1 = r * r0 by A3, XCMPLX_1:87;

now

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

suppose A6: 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 A7: 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 A8: x in dom (r (#) f) by Def6;
A9: f . x < R_EAL r0 by A7, Def12;
A10: r1 in REAL by XREAL_0:def 1;
then f . x < (R_EAL r1) / (R_EAL r) by A9, EXTREAL1:6;
then A11: (f . x) * (R_EAL r) < ((R_EAL r1) / (R_EAL r)) * (R_EAL r) by A6, XXREAL_3:72;
(R_EAL r1) / (R_EAL r) = r1 / r by A10, EXTREAL1:2;
then A12: ((R_EAL r1) / (R_EAL r)) * (R_EAL r) = (r1 / r) * r by EXTREAL1:1
.= r1 / (r / r) by XCMPLX_1:81
.= r1 / 1 by A3, XCMPLX_1:60
.= r1 ;
(r (#) f) . x = (R_EAL r) * (f . x) by A8, Def6;
hence x in less_dom ((r (#) f),(R_EAL r1)) by A8, A11, A12, Def12; :: thesis: verum

end;

then A13: less_dom (f,(R_EAL r0)) c= less_dom ((r (#) f),(R_EAL r1)) by SUBSET_1:2;
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 A14: x in less_dom ((r (#) f),(R_EAL r1)) ; :: thesis: x in less_dom (f,(R_EAL r0))
then A15: x in dom (r (#) f) by Def12;
(r (#) f) . x < R_EAL r1 by A14, Def12;
then (r (#) f) . x < (R_EAL r) * (R_EAL r0) by A5, EXTREAL1:5;
then A16: ((r (#) f) . x) / (R_EAL r) < ((R_EAL r) * (R_EAL r0)) / (R_EAL r) by A6, XXREAL_3:80;
(R_EAL r) * (R_EAL r0) = r * r0 by EXTREAL1:1;
then A17: ((R_EAL r) * (R_EAL r0)) / (R_EAL r) = (r * r0) / r by EXTREAL1:2
.= r0 / (r / r) by XCMPLX_1:77
.= r0 / 1 by A3, XCMPLX_1:60
.= r0 ;
( x in dom f & f . x = ((r (#) f) . x) / (R_EAL r) ) by A3, A15, Def6, Th6;
hence x in less_dom (f,(R_EAL r0)) by A16, A17, Def12; :: thesis: verum

end;

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

end;

suppose A18: 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 A19: 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 A20: x in dom (r (#) f) by Def6;
R_EAL r0 < f . x by A19, Def14;
then (R_EAL r1) / (R_EAL r) < f . x by A4, EXTREAL1:6;
then A21: (f . x) * (R_EAL r) < ((R_EAL r1) / (R_EAL r)) * (R_EAL r) by A18, XXREAL_3:102;
(R_EAL r1) / (R_EAL r) = r1 / r by A4, EXTREAL1:2;
then A22: ((R_EAL r1) / (R_EAL r)) * (R_EAL r) = (r1 / r) * r by EXTREAL1:1
.= r1 / (r / r) by XCMPLX_1:81
.= r1 / 1 by A3, XCMPLX_1:60
.= r1 ;
(r (#) f) . x = (R_EAL r) * (f . x) by A20, Def6;
hence x in less_dom ((r (#) f),(R_EAL r1)) by A20, A21, A22, Def12; :: thesis: verum

end;

then A23: great_dom (f,(R_EAL r0)) c= less_dom ((r (#) f),(R_EAL r1)) by SUBSET_1:2;
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 A24: x in less_dom ((r (#) f),(R_EAL r1)) ; :: thesis: x in great_dom (f,(R_EAL r0))
then A25: x in dom (r (#) f) by Def12;
(r (#) f) . x < R_EAL r1 by A24, Def12;
then (r (#) f) . x < (R_EAL r) * (R_EAL r0) by A5, EXTREAL1:5;
then A26: ((R_EAL r) * (R_EAL r0)) / (R_EAL r) < ((r (#) f) . x) / (R_EAL r) by A18, XXREAL_3:104;
(R_EAL r) * (R_EAL r0) = r * r0 by EXTREAL1:1;
then A27: ((R_EAL r) * (R_EAL r0)) / (R_EAL r) = (r * r0) / r by EXTREAL1:2
.= r0 / (r / r) by XCMPLX_1:77
.= r0 / 1 by A3, XCMPLX_1:60
.= r0 ;
( x in dom f & f . x = ((r (#) f) . x) / (R_EAL r) ) by A3, A25, Def6, Th6;
hence x in great_dom (f,(R_EAL r0)) by A26, A27, Def14; :: thesis: verum

end;

then less_dom ((r (#) f),(R_EAL r1)) c= great_dom (f,(R_EAL r0)) by SUBSET_1:2;
then great_dom (f,(R_EAL r0)) = less_dom ((r (#) f),(R_EAL r1)) by A23, 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 A28: r = 0 ; :: thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S

now

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

suppose A29: 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 A30: 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, A30;
then A31: x1 in dom (r (#) f) by Def6;
reconsider y = (r (#) f) . x1 as R_eal ;
y = (R_EAL r) * (f . x1) by A31, Def6
.= 0. by A28 ;
then x1 in less_dom ((r (#) f),(R_EAL r1)) by A29, A31, Def12;
hence x1 in A /\ (less_dom ((r (#) f),(R_EAL r1))) by A30, 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 A32: 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
A33: x1 in less_dom ((r (#) f),(R_EAL r1)) by SUBSET_1:4;
A34: x1 in dom (r (#) f) by A33, Def12;
A35: (r (#) f) . x1 < R_EAL r1 by A33, Def12;
A36: (r (#) f) . x1 in rng (r (#) f) by A34, FUNCT_1:def 3;
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
A37: ( x in dom (r (#) f) & y = (r (#) f) . x ) by PARTFUN1:3;
y = (R_EAL r) * (f . x) by A37, Def6
.= 0. by A28 ;
hence not y < R_EAL r1 by A32; :: thesis: verum

end;

hence contradiction by A35, A36; :: thesis: verum

end;

hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S by PROB_1:4; :: 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