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

let x be object ; :: thesis: ( x in { g where g is PartFunc of X,REAL : ( g in L1_Functions M & f in L1_Functions M & f a.e.= g,M ) } implies x in L1_Functions M )
assume x in { g where g is PartFunc of X,REAL : ( g in L1_Functions M & f in L1_Functions M & f a.e.= g,M ) } ; :: thesis: x in L1_Functions M
then ex g being PartFunc of X,REAL st
( x = g & g in L1_Functions M & f in L1_Functions M & f a.e.= g,M ) ;
hence x in L1_Functions M ; :: thesis: verum

end;

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