let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S holds zeroCoset M = zeroCoset (M,1)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds zeroCoset M = zeroCoset (M,1)

let M be sigma_Measure of S; :: thesis: zeroCoset M = zeroCoset (M,1)

reconsider z = zeroCoset (M,1) as Element of CosetSet M by Th71;

X --> 0 in Lp_Functions (M,1) by Th23;

then ex E being Element of S st

( M . (E `) = 0 & dom (X --> 0) = E & X --> 0 is E -measurable ) by Th35;

then A1: z = a.e-eq-class ((X --> 0),M) by Lm12;

X --> 0 in L1_Functions M by Th56;

hence zeroCoset M = zeroCoset (M,1) by A1, LPSPACE1:def 16; :: thesis: verum

for M being sigma_Measure of S holds zeroCoset M = zeroCoset (M,1)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds zeroCoset M = zeroCoset (M,1)

let M be sigma_Measure of S; :: thesis: zeroCoset M = zeroCoset (M,1)

reconsider z = zeroCoset (M,1) as Element of CosetSet M by Th71;

X --> 0 in Lp_Functions (M,1) by Th23;

then ex E being Element of S st

( M . (E `) = 0 & dom (X --> 0) = E & X --> 0 is E -measurable ) by Th35;

then A1: z = a.e-eq-class ((X --> 0),M) by Lm12;

X --> 0 in L1_Functions M by Th56;

hence zeroCoset M = zeroCoset (M,1) by A1, LPSPACE1:def 16; :: thesis: verum