A1: now

let x be set ; :: thesis: ( x in { f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0 ,M ) } implies x in the carrier of (RLSp_L1Funct M) )
assume x in { f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0 ,M ) } ; :: thesis: x in the carrier of (RLSp_L1Funct M)
then ex f being PartFunc of X,REAL st
( x = f & f in L1_Functions M & f a.e.= X --> 0 ,M ) ;
hence x in the carrier of (RLSp_L1Funct M) ; :: thesis: verum

end;

( X --> 0 a.e.= X --> 0 ,M & X --> 0 in L1_Functions M ) by Lm3, Th28;
then X --> 0 in { f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0 ,M ) } ;
hence { f where f is PartFunc of X,REAL : ( f in L1_Functions M & f a.e.= X --> 0 ,M ) } is non empty Subset of (RLSp_L1Funct M) by A1, TARSKI:def 3; :: thesis: verum