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 A -measurable & A c= dom f holds
r (#) f is A -measurable
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 A -measurable & A c= dom f holds
r (#) f is A -measurable
let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S
for r being Real st f is A -measurable & A c= dom f holds
r (#) f is A -measurable
let A be Element of S; :: thesis: for r being Real st f is A -measurable & A c= dom f holds
r (#) f is A -measurable
let r be Real; :: thesis: ( f is A -measurable & A c= dom f implies r (#) f is A -measurable )
assume that
A1: f is A -measurable and
A2: A c= dom f ; :: thesis: r (#) f is A -measurable
for r1 being Real holds A /\ (less_dom ((r (#) f),r1)) in S

proof

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

now :: thesis: A /\ (less_dom ((r (#) f),r1)) in S

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

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

reconsider r0 = r1 / r as Real ;
A4: r1 = r * r0 by A3, XCMPLX_1:87;

now :: thesis: A /\ (less_dom ((r (#) f),r1)) in S

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

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

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

proof

let x be Element of X; :: thesis: ( x in less_dom (f,r0) implies x in less_dom ((r (#) f),r1) )
assume A6: x in less_dom (f,r0) ; :: thesis: x in less_dom ((r (#) f),r1)
then x in dom f by Def11;
then A7: x in dom (r (#) f) by Def6;
A8: f . x < r0 by A6, Def11;
f . x < r1 / r by A8;
then A9: (f . x) * r < (r1 / r) * r by A5, XXREAL_3:72;
A10: (r1 / r) * r = (r1 / r) * r
.= r1 / (r / r) by XCMPLX_1:81
.= r1 / 1 by A3, XCMPLX_1:60
.= r1 ;
(r (#) f) . x = r * (f . x) by A7, Def6;
hence x in less_dom ((r (#) f),r1) by A7, A9, A10, Def11; :: thesis: verum

end;

then A11: less_dom (f,r0) c= less_dom ((r (#) f),r1) ;
for x being Element of X st x in less_dom ((r (#) f),r1) holds
x in less_dom (f,r0)

proof

let x be Element of X; :: thesis: ( x in less_dom ((r (#) f),r1) implies x in less_dom (f,r0) )
assume A12: x in less_dom ((r (#) f),r1) ; :: thesis: x in less_dom (f,r0)
then A13: x in dom (r (#) f) by Def11;
(r (#) f) . x < r1 by A12, Def11;
then (r (#) f) . x < r * r0 by A4;
then A14: ((r (#) f) . x) / r < (r * r0) / r by A5, XXREAL_3:80;
A15: (r * r0) / r = (r * r0) / r
.= 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 ) by A3, A13, Def6, Th6;
hence x in less_dom (f,r0) by A14, A15, Def11; :: thesis: verum

end;

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

end;

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

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

proof

let x be Element of X; :: thesis: ( x in great_dom (f,r0) implies x in less_dom ((r (#) f),r1) )
assume A17: x in great_dom (f,r0) ; :: thesis: x in less_dom ((r (#) f),r1)
then x in dom f by Def13;
then A18: x in dom (r (#) f) by Def6;
r0 < f . x by A17, Def13;
then r1 / r < f . x ;
then A19: (f . x) * r < (r1 / r) * r by A16, XXREAL_3:102;
A20: (r1 / r) * r = (r1 / r) * r
.= r1 / (r / r) by XCMPLX_1:81
.= r1 / 1 by A3, XCMPLX_1:60
.= r1 ;
(r (#) f) . x = r * (f . x) by A18, Def6;
hence x in less_dom ((r (#) f),r1) by A18, A19, A20, Def11; :: thesis: verum

end;

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

proof

let x be Element of X; :: thesis: ( x in less_dom ((r (#) f),r1) implies x in great_dom (f,r0) )
assume A22: x in less_dom ((r (#) f),r1) ; :: thesis: x in great_dom (f,r0)
then A23: x in dom (r (#) f) by Def11;
(r (#) f) . x < r1 by A22, Def11;
then (r (#) f) . x < r * r0 by A4;
then A24: (r * r0) / r < ((r (#) f) . x) / r by A16, XXREAL_3:104;
A25: (r * r0) / r = (r * r0) / r
.= 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 ) by A3, A23, Def6, Th6;
hence x in great_dom (f,r0) by A24, A25, Def13; :: thesis: verum

end;

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

end;

end;

end;

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

end;

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

now :: thesis: A /\ (less_dom ((r (#) f),r1)) in S

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

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

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

proof

let x1 be object ; :: thesis: ( x1 in A implies x1 in A /\ (less_dom ((r (#) f),r1)) )
assume A28: x1 in A ; :: thesis: x1 in A /\ (less_dom ((r (#) f),r1))
then reconsider x1 = x1 as Element of X ;
x1 in dom f by A2, A28;
then A29: x1 in dom (r (#) f) by Def6;
reconsider y = (r (#) f) . x1 as R_eal ;
y = r * (f . x1) by A29, Def6
.= 0. by A26 ;
then x1 in less_dom ((r (#) f),r1) by A27, A29, Def11;
hence x1 in A /\ (less_dom ((r (#) f),r1)) by A28, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

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

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

proof

assume less_dom ((r (#) f),r1) <> {} ; :: thesis: contradiction
then consider x1 being Element of X such that
A31: x1 in less_dom ((r (#) f),r1) by SUBSET_1:4;
A32: x1 in dom (r (#) f) by A31, Def11;
A33: (r (#) f) . x1 < r1 by A31, Def11;
A34: (r (#) f) . x1 in rng (r (#) f) by A32, FUNCT_1:def 3;
for y being R_eal st y in rng (r (#) f) holds
not y < r1

proof

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

end;

hence contradiction by A33, A34; :: thesis: verum

end;

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

end;

end;

end;

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

end;

end;

end;

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

end;

hence r (#) f is A -measurable ; :: thesis: verum