A1:
now 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 ;
( 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 ) }
;
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))
;
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; verum