now :: thesis: for x being object st x in { g where g is PartFunc of X,REAL : ( g in Lp_Functions (M,k) & f a.e.= g,M ) } holds

x in Lp_Functions (M,k)

hence
{ h where h is PartFunc of X,REAL : ( h in Lp_Functions (M,k) & f a.e.= h,M ) } is Subset of (Lp_Functions (M,k))
by TARSKI:def 3; :: thesis: verumx in Lp_Functions (M,k)

let x be object ; :: thesis: ( x in { g where g is PartFunc of X,REAL : ( g in Lp_Functions (M,k) & f a.e.= g,M ) } implies x in Lp_Functions (M,k) )

assume x in { g where g is PartFunc of X,REAL : ( g in Lp_Functions (M,k) & f a.e.= g,M ) } ; :: thesis: x in Lp_Functions (M,k)

then ex g being PartFunc of X,REAL st

( x = g & g in Lp_Functions (M,k) & f a.e.= g,M ) ;

hence x in Lp_Functions (M,k) ; :: thesis: verum

end;assume x in { g where g is PartFunc of X,REAL : ( g in Lp_Functions (M,k) & f a.e.= g,M ) } ; :: thesis: x in Lp_Functions (M,k)

then ex g being PartFunc of X,REAL st

( x = g & g in Lp_Functions (M,k) & f a.e.= g,M ) ;

hence x in Lp_Functions (M,k) ; :: thesis: verum