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