A1: now :: thesis: for x being object st x in { f where f is PartFunc of X,COMPLEX : ( f in L1_CFunctions M & f a.e.cpfunc= X --> 0c,M ) } holds
x in the carrier of (CLSp_L1Funct M)

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

end;

( X --> 0c a.e.cpfunc= X --> 0c,M & X --> 0 in L1_CFunctions M ) by Lm3, Th22;
then X --> 0 in { f where f is PartFunc of X,COMPLEX : ( f in L1_CFunctions M & f a.e.cpfunc= X --> 0c,M ) } ;
hence { f where f is PartFunc of X,COMPLEX : ( f in L1_CFunctions M & f a.e.cpfunc= X --> 0c,M ) } is non empty Subset of (CLSp_L1Funct M) by A1, TARSKI:def 3; :: thesis: verum