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