let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real holds
( 0. (RLSp_LpFunct (M,k)) = X --> 0 & 0. (RLSp_LpFunct (M,k)) in AlmostZeroLpFunctions (M,k) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for k being positive Real holds
( 0. (RLSp_LpFunct (M,k)) = X --> 0 & 0. (RLSp_LpFunct (M,k)) in AlmostZeroLpFunctions (M,k) )
let M be sigma_Measure of S; :: thesis: for k being positive Real holds
( 0. (RLSp_LpFunct (M,k)) = X --> 0 & 0. (RLSp_LpFunct (M,k)) in AlmostZeroLpFunctions (M,k) )
let k be positive Real; :: thesis: ( 0. (RLSp_LpFunct (M,k)) = X --> 0 & 0. (RLSp_LpFunct (M,k)) in AlmostZeroLpFunctions (M,k) )
thus 0. (RLSp_LpFunct (M,k)) = X --> 0 by Th23, SUBSET_1:def 8; :: thesis: 0. (RLSp_LpFunct (M,k)) in AlmostZeroLpFunctions (M,k)
A1: ( X --> 0 a.e.= X --> 0,M & X --> 0 in Lp_Functions (M,k) ) by Th23, LPSPACE1:28;
0. (RLSp_LpFunct (M,k)) = 0. (RLSp_PFunct X) by Th23, SUBSET_1:def 8;
hence 0. (RLSp_LpFunct (M,k)) in AlmostZeroLpFunctions (M,k) by A1; :: thesis: verum