let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S holds
( 0. (RLSp_L1Funct M) = X --> 0 & 0. (RLSp_L1Funct M) in AlmostZeroFunctions M )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds
( 0. (RLSp_L1Funct M) = X --> 0 & 0. (RLSp_L1Funct M) in AlmostZeroFunctions M )
let M be sigma_Measure of S; :: thesis: ( 0. (RLSp_L1Funct M) = X --> 0 & 0. (RLSp_L1Funct M) in AlmostZeroFunctions M )
thus 0. (RLSp_L1Funct M) = X --> 0 by LmDef1, FUNCT_7:def 1; :: thesis: 0. (RLSp_L1Funct M) in AlmostZeroFunctions M
A2: ( X --> 0 a.e.= X --> 0 ,M & X --> 0 in L1_Functions M ) by Th04, LmDef1;
0. (RLSp_L1Funct M) = 0. (RLSp_PFunct X) by LmDef1, FUNCT_7:def 1;
hence 0. (RLSp_L1Funct M) in AlmostZeroFunctions M by A2; :: thesis: verum