set z = ZeroMap (M,M);
set H = { f where f is Function of M,M : f is Endomorphism of M } ;

A1: now :: thesis: for u being object st u in { f where f is Function of M,M : f is Endomorphism of M } holds
u in Funcs ( the carrier of M, the carrier of M)

let u be object ; :: thesis: ( u in { f where f is Function of M,M : f is Endomorphism of M } implies u in Funcs ( the carrier of M, the carrier of M) )
assume u in { f where f is Function of M,M : f is Endomorphism of M } ; :: thesis: u in Funcs ( the carrier of M, the carrier of M)
then ex z being Function of M,M st
( u = z & z is Endomorphism of M ) ;
hence u in Funcs ( the carrier of M, the carrier of M) by FUNCT_2:8; :: thesis: verum

end;

ZeroMap (M,M) in { f where f is Function of M,M : f is Endomorphism of M } ;
hence { f where f is Function of M,M : f is Endomorphism of M } is non empty Subset of (Funcs ( the carrier of M, the carrier of M)) by A1, TARSKI:def 3; :: thesis: verum