let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL
for r being Real st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable holds
( Integral1 (M1,(r (#) f)) = r (#) (Integral1 (M1,f)) & Integral2 (M2,(r (#) f)) = r (#) (Integral2 (M2,f)) )
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL
for r being Real st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable holds
( Integral1 (M1,(r (#) f)) = r (#) (Integral1 (M1,f)) & Integral2 (M2,(r (#) f)) = r (#) (Integral2 (M2,f)) )
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL
for r being Real st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable holds
( Integral1 (M1,(r (#) f)) = r (#) (Integral1 (M1,f)) & Integral2 (M2,(r (#) f)) = r (#) (Integral2 (M2,f)) )
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL
for r being Real st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable holds
( Integral1 (M1,(r (#) f)) = r (#) (Integral1 (M1,f)) & Integral2 (M2,(r (#) f)) = r (#) (Integral2 (M2,f)) )
let M2 be sigma_Measure of S2; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL
for r being Real st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable holds
( Integral1 (M1,(r (#) f)) = r (#) (Integral1 (M1,f)) & Integral2 (M2,(r (#) f)) = r (#) (Integral2 (M2,f)) )
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL
for r being Real st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable holds
( Integral1 (M1,(r (#) f)) = r (#) (Integral1 (M1,f)) & Integral2 (M2,(r (#) f)) = r (#) (Integral2 (M2,f)) )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: for r being Real st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable holds
( Integral1 (M1,(r (#) f)) = r (#) (Integral1 (M1,f)) & Integral2 (M2,(r (#) f)) = r (#) (Integral2 (M2,f)) )
let r be Real; :: thesis: ( E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable implies ( Integral1 (M1,(r (#) f)) = r (#) (Integral1 (M1,f)) & Integral2 (M2,(r (#) f)) = r (#) (Integral2 (M2,f)) ) )
assume that
A1: E = dom f and
A2: ( f is nonnegative or f is nonpositive ) and
A3: f is E -measurable ; :: thesis: ( Integral1 (M1,(r (#) f)) = r (#) (Integral1 (M1,f)) & Integral2 (M2,(r (#) f)) = r (#) (Integral2 (M2,f)) )
A4: ( dom (r (#) (Integral1 (M1,f))) = X2 & dom (r (#) (Integral2 (M2,f))) = X1 ) by FUNCT_2:def 1;
now :: thesis: for y being Element of X2 holds (Integral1 (M1,(r (#) f))) . y = (r (#) (Integral1 (M1,f))) . y
let y be Element of X2; :: thesis: (Integral1 (M1,(r (#) f))) . y = (r (#) (Integral1 (M1,f))) . y
dom (ProjPMap2 (f,y)) = Y-section (E,y) by A1, Def4;
then A5: dom (ProjPMap2 (f,y)) = Measurable-Y-section (E,y) by MEASUR11:def 7;
A6: ( ProjPMap2 (f,y) is nonnegative or ProjPMap2 (f,y) is nonpositive ) by A2, Th32, Th33;
(Integral1 (M1,(r (#) f))) . y = Integral (M1,(ProjPMap2 ((r (#) f),y))) by Def7
.= Integral (M1,(r (#) (ProjPMap2 (f,y)))) by Th29
.= r * (Integral (M1,(ProjPMap2 (f,y)))) by A5, A6, A1, A3, Th47, Lm1, Lm2
.= r * ((Integral1 (M1,f)) . y) by Def7 ;
hence (Integral1 (M1,(r (#) f))) . y = (r (#) (Integral1 (M1,f))) . y by A4, MESFUNC1:def 6; :: thesis: verum
end;
hence Integral1 (M1,(r (#) f)) = r (#) (Integral1 (M1,f)) by FUNCT_2:def 8; :: thesis: Integral2 (M2,(r (#) f)) = r (#) (Integral2 (M2,f))
now :: thesis: for x being Element of X1 holds (Integral2 (M2,(r (#) f))) . x = (r (#) (Integral2 (M2,f))) . x
let x be Element of X1; :: thesis: (Integral2 (M2,(r (#) f))) . x = (r (#) (Integral2 (M2,f))) . x
dom (ProjPMap1 (f,x)) = X-section (E,x) by A1, Def3;
then B5: dom (ProjPMap1 (f,x)) = Measurable-X-section (E,x) by MEASUR11:def 6;
B6: ( ProjPMap1 (f,x) is nonnegative or ProjPMap1 (f,x) is nonpositive ) by A2, Th32, Th33;
(Integral2 (M2,(r (#) f))) . x = Integral (M2,(ProjPMap1 ((r (#) f),x))) by Def8
.= Integral (M2,(r (#) (ProjPMap1 (f,x)))) by Th29
.= r * (Integral (M2,(ProjPMap1 (f,x)))) by B6, B5, A1, A3, Th47, Lm1, Lm2
.= r * ((Integral2 (M2,f)) . x) by Def8 ;
hence (Integral2 (M2,(r (#) f))) . x = (r (#) (Integral2 (M2,f))) . x by A4, MESFUNC1:def 6; :: thesis: verum
end;
hence Integral2 (M2,(r (#) f)) = r (#) (Integral2 (M2,f)) by FUNCT_2:def 8; :: thesis: verum