X --> 0 in L1_Functions M by Lm3;
then a.e-eq-class ((X --> 0),M) in CosetSet M ;
hence ( ex b₁ being Element of CosetSet M ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b₁ = a.e-eq-class (f,M) ) & ( for b₁, b₂ being Element of CosetSet M st ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b₁ = a.e-eq-class (f,M) ) & ex f being PartFunc of X,REAL st
( f = X --> 0 & f in L1_Functions M & b₂ = a.e-eq-class (f,M) ) holds
b₁ = b₂ ) ) by Lm3; :: thesis: verum