A1: now

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

end;

A3: X --> 0 a.e.= X --> 0 ,M by LPSPACE1:28;
X --> 0 in Lp_Functions M,k by LmDef1Lp;
then X --> 0 in { f where f is PartFunc of X,REAL : ( f in Lp_Functions M,k & f a.e.= X --> 0 ,M ) } by A3;
hence { f where f is PartFunc of X,REAL : ( f in Lp_Functions M,k & f a.e.= X --> 0 ,M ) } is non empty Subset of (RLSp_LpFunct M,k) by A1, TARSKI:def 3; :: thesis: verum