theorem Th1: :: FLEXARY1:1

for F being Function-yielding Function
for a being object holds
( a in Values F iff ex x, y being object st
( x in dom F & y in dom (F . x) & a = (F . x) . y ) )