A1: now :: thesis: for x being object st x in { f where f is PartFunc of X,REAL : ( f in Lp_Functions (M,k) & f a.e.= X --> 0,M ) } holds
x in the carrier of (RLSp_LpFunct (M,k))

let x be object ; :: 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;

A2: X --> 0 a.e.= X --> 0,M by LPSPACE1:28;
X --> 0 in Lp_Functions (M,k) by Th23;
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 A2;
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