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))

A2:
X --> 0 a.e.= X --> 0,M
by LPSPACE1:28;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;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

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