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 LmDef1Lp, FUNCT_7:def 1; :: thesis: 0. (RLSp_LpFunct M,k) in AlmostZeroLpFunctions M,k
A2: ( X --> 0 a.e.= X --> 0 ,M & X --> 0 in Lp_Functions M,k ) by LmDef1Lp, LPSPACE1:28;
0. (RLSp_LpFunct M,k) = 0. (RLSp_PFunct X) by LmDef1Lp, FUNCT_7:def 1;
hence 0. (RLSp_LpFunct M,k) in AlmostZeroLpFunctions M,k by A2; :: thesis: verum