not dom G is empty ;
then reconsider f = rngs G as non-empty non empty Function by FUNCT_6:60, RELAT_1:38;
not Union f is empty ;
hence not Values G is empty by MATRIX_0:def 9; :: thesis: verum