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 Lm3, FUNCT_7:def 1; :: thesis: 0. (RLSp_L1Funct M) in AlmostZeroFunctions M
( X --> 0 a.e.= X --> 0,M & 0. (RLSp_L1Funct M) = 0. (RLSp_PFunct X) ) by Lm3, Th28, FUNCT_7:def 1;
hence 0. (RLSp_L1Funct M) in AlmostZeroFunctions M ; :: thesis: verum