let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S holds
( 0. (CLSp_L1Funct M) = X --> 0c & 0. (CLSp_L1Funct M) in AlmostZeroCFunctions M )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds
( 0. (CLSp_L1Funct M) = X --> 0c & 0. (CLSp_L1Funct M) in AlmostZeroCFunctions M )
let M be sigma_Measure of S; :: thesis: ( 0. (CLSp_L1Funct M) = X --> 0c & 0. (CLSp_L1Funct M) in AlmostZeroCFunctions M )
thus 0. (CLSp_L1Funct M) = X --> 0c by Lm3, SUBSET_1:def 8; :: thesis: 0. (CLSp_L1Funct M) in AlmostZeroCFunctions M
( X --> 0c a.e.cpfunc= X --> 0c,M & 0. (CLSp_L1Funct M) = 0. (CLSp_PFunct X) ) by Lm3, Th22, SUBSET_1:def 8;
hence 0. (CLSp_L1Funct M) in AlmostZeroCFunctions M ; :: thesis: verum