dom (rngs M) = dom M by FUNCT_6:60;
then reconsider X = rng (rngs M) as non empty with_non-empty_elements set by RELAT_1:42;
Values M = Union (rngs M) by MATRIX_0:def 9
.= union X by CARD_3:def 4 ;
hence not Values M is empty ; :: thesis: verum