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
A3: 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

A4: 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;

A8: 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

A10: 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)
A12: x in dom f by A11, Def12;
A13: x in dom (r (#) f) by A12, Def6;
A14: f . x < R_EAL r0 by A11, Def12;
A15: r1 in REAL by XREAL_0:def 1;
A16: f . x < (R_EAL r1) / (R_EAL r) by A14, A15, EXTREAL1:39;
A17: (f . x) * (R_EAL r) < ((R_EAL r1) / (R_EAL r)) * (R_EAL r) by A9, A16, XXREAL_3:83;
A18: (R_EAL r1) / (R_EAL r) = r1 / r by A15, EXTREAL1:32;
A19: ((R_EAL r1) / (R_EAL r)) * (R_EAL r) = (r1 / r) * r by A18, EXTREAL1:13
.= r1 / (r / r) by XCMPLX_1:82
.= r1 / 1 by A5, XCMPLX_1:60
.= r1 ;
A20: (r (#) f) . x = (R_EAL r) * (f . x) by A13, Def6;
thus x in less_dom (r (#) f),(R_EAL r1) by A13, A17, A19, A20, Def12; :: thesis: verum

end;

A21: less_dom f,(R_EAL r0) c= less_dom (r (#) f),(R_EAL r1) by A10, SUBSET_1:7;
A22: 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)
A24: x in dom (r (#) f) by A23, Def12;
A25: (r (#) f) . x < R_EAL r1 by A23, Def12;
A26: (r (#) f) . x < (R_EAL r) * (R_EAL r0) by A7, A25, EXTREAL1:38;
A27: ((r (#) f) . x) / (R_EAL r) < ((R_EAL r) * (R_EAL r0)) / (R_EAL r) by A9, A26, XXREAL_3:91;
A28: (R_EAL r) * (R_EAL r0) = r * r0 by EXTREAL1:13;
A29: ((R_EAL r) * (R_EAL r0)) / (R_EAL r) = (r * r0) / r by A28, EXTREAL1:32
.= r0 / (r / r) by XCMPLX_1:78
.= r0 / 1 by A5, XCMPLX_1:60
.= r0 ;
A30: ( x in dom f & f . x = ((r (#) f) . x) / (R_EAL r) ) by A5, A24, Def6, Th6;
thus x in less_dom f,(R_EAL r0) by A27, A29, A30, Def12; :: thesis: verum

end;

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

end;

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

A34: 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)
A36: x in dom f by A35, Def14;
A37: x in dom (r (#) f) by A36, Def6;
A38: R_EAL r0 < f . x by A35, Def14;
A39: (R_EAL r1) / (R_EAL r) < f . x by A6, A38, EXTREAL1:39;
A40: (f . x) * (R_EAL r) < ((R_EAL r1) / (R_EAL r)) * (R_EAL r) by A33, A39, XXREAL_3:114;
A41: (R_EAL r1) / (R_EAL r) = r1 / r by A6, EXTREAL1:32;
A42: ((R_EAL r1) / (R_EAL r)) * (R_EAL r) = (r1 / r) * r by A41, EXTREAL1:13
.= r1 / (r / r) by XCMPLX_1:82
.= r1 / 1 by A5, XCMPLX_1:60
.= r1 ;
A43: (r (#) f) . x = (R_EAL r) * (f . x) by A37, Def6;
thus x in less_dom (r (#) f),(R_EAL r1) by A37, A40, A42, A43, Def12; :: thesis: verum

end;

A44: great_dom f,(R_EAL r0) c= less_dom (r (#) f),(R_EAL r1) by A34, SUBSET_1:7;
A45: 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)
A47: x in dom (r (#) f) by A46, Def12;
A48: (r (#) f) . x < R_EAL r1 by A46, Def12;
A49: (r (#) f) . x < (R_EAL r) * (R_EAL r0) by A7, A48, EXTREAL1:38;
A50: ((R_EAL r) * (R_EAL r0)) / (R_EAL r) < ((r (#) f) . x) / (R_EAL r) by A33, A49, XXREAL_3:116;
A51: (R_EAL r) * (R_EAL r0) = r * r0 by EXTREAL1:13;
A52: ((R_EAL r) * (R_EAL r0)) / (R_EAL r) = (r * r0) / r by A51, EXTREAL1:32
.= r0 / (r / r) by XCMPLX_1:78
.= r0 / 1 by A5, XCMPLX_1:60
.= r0 ;
A53: ( x in dom f & f . x = ((r (#) f) . x) / (R_EAL r) ) by A5, A47, Def6, Th6;
thus x in great_dom f,(R_EAL r0) by A50, A52, A53, Def14; :: thesis: verum

end;

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

end;

end;

end;

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

end;

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

A57: now

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

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

A59: 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))
reconsider x1 = x1 as Element of X by A60;
A61: x1 in dom f by A2, A60;
A62: x1 in dom (r (#) f) by A61, Def6;
reconsider y = (r (#) f) . x1 as R_eal ;
A63: y = (R_EAL r) * (f . x1) by A62, Def6
.= 0. by A56 ;
A64: x1 in less_dom (r (#) f),(R_EAL r1) by A58, A62, A63, Def12;
thus x1 in A /\ (less_dom (r (#) f),(R_EAL r1)) by A60, A64, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

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

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

proof

assume A69: less_dom (r (#) f),(R_EAL r1) <> {} ; :: thesis: contradiction
consider x1 being Element of X such that
A70: x1 in less_dom (r (#) f),(R_EAL r1) by A69, 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;
A74: 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 A75: y in rng (r (#) f) ; :: thesis: not y < R_EAL r1
consider x being Element of X such that
A76: ( x in dom (r (#) f) & y = (r (#) f) . x ) by A75, PARTFUN1:26;
A77: y = (R_EAL r) * (f . x) by A76, Def6
.= 0. by A56 ;
thus not y < R_EAL r1 by A67, A77; :: thesis: verum

end;

thus contradiction by A72, A73, A74; :: thesis: verum

end;

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

end;

end;

end;

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

end;

end;

end;

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

end;

thus r (#) f is_measurable_on A by A3, Def17; :: thesis: verum