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 Th9a;
X --> 0 in Lp_Functions M,1 by LmDef1Lp;
then ex E being Element of S st
( M . (E ` ) = 0 & dom (X --> 0 ) = E & X --> 0 is_measurable_on E ) by EQC00a;
then A3: z = a.e-eq-class (X --> 0 ),M by Lem03;
X --> 0 in L1_Functions M by LmDef1;
hence zeroCoset M = zeroCoset M,1 by A3, LPSPACE1:def 16; :: thesis: verum