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, SUBSET_1:def 8; :: 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, SUBSET_1:def 8;
hence 0. (RLSp_L1Funct M) in AlmostZeroFunctions M ; :: thesis: verum