X --> 0 in Lp_Functions M,k by LmDef1Lp;
then a.e-eq-class_Lp (X --> 0 ),M,k in CosetSet M,k ;
hence a.e-eq-class_Lp (X --> 0 ),M,k is Element of CosetSet M,k ; :: thesis: verum