ZeroMap (M,M) in set_End M ;
hence ZeroMap (M,M) is Element of set_End M ; :: thesis: verum