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

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

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

end;

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