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

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

end;

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