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

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

now

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

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

less_dom f,(R_EAL r0) = less_dom (r (#) f),(R_EAL r1)

proof

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 A6: x in less_dom f,(R_EAL r0) ; :: thesis: x in less_dom (r (#) f),(R_EAL r1)
then ( x in dom f & f . x < R_EAL r0 ) by Def12;
then A7: x in dom (r (#) f) by Def6;
A8: f . x < R_EAL r0 by A6, Def12;
A9: r1 in REAL by XREAL_0:def 1;
then f . x < (R_EAL r1) / (R_EAL r) by A8, EXTREAL1:39;
then A10: (f . x) * (R_EAL r) < ((R_EAL r1) / (R_EAL r)) * (R_EAL r) by A5, XXREAL_3:83;
(R_EAL r1) / (R_EAL r) = r1 / r by A9, EXTREAL1:32;
then A11: ((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 A2, XCMPLX_1:60
.= r1 ;
(r (#) f) . x = (R_EAL r) * (f . x) by A7, Def6;
hence x in less_dom (r (#) f),(R_EAL r1) by A7, A10, A11, Def12; :: thesis: verum

end;

then A12: 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 A13: x in less_dom (r (#) f),(R_EAL r1) ; :: thesis: x in less_dom f,(R_EAL r0)
then A14: ( x in dom (r (#) f) & (r (#) f) . x < R_EAL r1 ) by Def12;
then A15: x in dom f by Def6;
(r (#) f) . x < R_EAL r1 by A13, Def12;
then (r (#) f) . x < (R_EAL r) * (R_EAL r0) by A4, EXTREAL1:38;
then A16: ((r (#) f) . x) / (R_EAL r) < ((R_EAL r) * (R_EAL r0)) / (R_EAL r) by A5, XXREAL_3:91;
(R_EAL r) * (R_EAL r0) = r * r0 by EXTREAL1:13;
then A17: ((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 A2, XCMPLX_1:60
.= r0 ;
f . x = ((r (#) f) . x) / (R_EAL r) by A2, A14, Th6;
hence x in less_dom f,(R_EAL r0) by A15, A16, A17, Def12; :: thesis: verum

end;

then less_dom (r (#) f),(R_EAL r1) c= less_dom f,(R_EAL r0) by SUBSET_1:7;
hence less_dom f,(R_EAL r0) = less_dom (r (#) f),(R_EAL r1) by A12, XBOOLE_0:def 10; :: thesis: verum

end;

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

great_dom f,(R_EAL r0) = less_dom (r (#) f),(R_EAL r1)

proof

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 & R_EAL r0 < f . x ) 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 A3, EXTREAL1:39;
then A21: (f . x) * (R_EAL r) < ((R_EAL r1) / (R_EAL r)) * (R_EAL r) by A18, XXREAL_3:114;
(R_EAL r1) / (R_EAL r) = r1 / r by A3, EXTREAL1:32;
then A22: ((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 A2, 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: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 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) & (r (#) f) . x < R_EAL r1 ) by Def12;
then A26: x in dom f by Def6;
(r (#) f) . x < R_EAL r1 by A24, Def12;
then (r (#) f) . x < (R_EAL r) * (R_EAL r0) by A4, EXTREAL1:38;
then A27: ((R_EAL r) * (R_EAL r0)) / (R_EAL r) < ((r (#) f) . x) / (R_EAL r) by A18, XXREAL_3:116;
(R_EAL r) * (R_EAL r0) = r * r0 by EXTREAL1:13;
then A28: ((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 A2, XCMPLX_1:60
.= r0 ;
f . x = ((r (#) f) . x) / (R_EAL r) by A2, A25, Th6;
hence x in great_dom f,(R_EAL r0) by A26, A27, A28, Def14; :: thesis: verum

end;

then less_dom (r (#) f),(R_EAL r1) c= great_dom f,(R_EAL r0) by SUBSET_1:7;
hence great_dom f,(R_EAL r0) = less_dom (r (#) f),(R_EAL r1) by A23, XBOOLE_0:def 10; :: thesis: verum

end;

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

end;

end;

end;

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

end;

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

now

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

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

A /\ (less_dom (r (#) f),(R_EAL r1)) = A

proof

A31: A /\ (less_dom (r (#) f),(R_EAL r1)) c= A by XBOOLE_1:17;
A c= A /\ (less_dom (r (#) f),(R_EAL r1))

proof

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 A32: 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 A1, A32;
then A33: x1 in dom (r (#) f) by Def6;
reconsider y = (r (#) f) . x1 as R_eal ;
y = (R_EAL r) * (f . x1) by A33, Def6
.= 0. by A29 ;
then x1 in less_dom (r (#) f),(R_EAL r1) by A30, A33, Def12;
hence x1 in A /\ (less_dom (r (#) f),(R_EAL r1)) by A32, XBOOLE_0:def 4; :: thesis: verum

end;

hence A c= A /\ (less_dom (r (#) f),(R_EAL r1)) by TARSKI:def 3; :: thesis: verum

end;

hence A /\ (less_dom (r (#) f),(R_EAL r1)) = A by A31, XBOOLE_0:def 10; :: thesis: verum

end;

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

end;

suppose A34: 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
A35: x1 in less_dom (r (#) f),(R_EAL r1) by SUBSET_1:10;
A36: ( x1 in dom (r (#) f) & (r (#) f) . x1 < R_EAL r1 ) by A35, Def12;
A37: (r (#) f) . x1 < R_EAL r1 by A35, Def12;
A38: (r (#) f) . x1 in rng (r (#) f) by A36, 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
A39: ( x in dom (r (#) f) & y = (r (#) f) . x ) by PARTFUN1:26;
y = (R_EAL r) * (f . x) by A39, Def6
.= 0. by A29 ;
hence not y < R_EAL r1 by A34; :: thesis: verum

end;

hence contradiction by A37, A38; :: 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