:: deftheorem defines Values MATRIX_0:def 9 :
for F being Function-yielding Function holds Values F = Union (rngs F);