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