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

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