let a be Real; for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f a.e.= g,M holds
a (#) f a.e.= a (#) g,M
let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f a.e.= g,M holds
a (#) f a.e.= a (#) g,M
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f a.e.= g,M holds
a (#) f a.e.= a (#) g,M
let M be sigma_Measure of S; for f, g being PartFunc of X,REAL st f a.e.= g,M holds
a (#) f a.e.= a (#) g,M
let f, g be PartFunc of X,REAL; ( f a.e.= g,M implies a (#) f a.e.= a (#) g,M )
assume
f a.e.= g,M
; a (#) f a.e.= a (#) g,M
then consider E being Element of S such that
A1:
M . E = 0
and
A2:
f | (E `) = g | (E `)
;
(a (#) f) | (E `) =
a (#) (g | (E `))
by A2, RFUNCT_1:49
.=
(a (#) g) | (E `)
by RFUNCT_1:49
;
hence
a (#) f a.e.= a (#) g,M
by A1; verum