let F be Function-yielding Function; :: thesis: 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 ) )
let a be object ; :: thesis: ( a in Values F iff ex x, y being object st
( x in dom F & y in dom (F . x) & a = (F . x) . y ) )
A1: Values F = Union (rngs F) by MATRIX_0:def 9
.= union (rng (rngs F)) by CARD_3:def 4 ;
A2: dom (rngs F) = dom F by FUNCT_6:def 3;
thus ( a in Values F implies ex x, y being object st
( x in dom F & y in dom (F . x) & a = (F . x) . y ) ) :: thesis: ( ex x, y being object st
( x in dom F & y in dom (F . x) & a = (F . x) . y ) implies a in Values F )

proof

assume a in Values F ; :: thesis: ex x, y being object st
( x in dom F & y in dom (F . x) & a = (F . x) . y )
then consider y being set such that
A3: ( a in y & y in rng (rngs F) ) by A1, TARSKI:def 4;
consider z being object such that
A4: ( z in dom (rngs F) & (rngs F) . z = y ) by A3, FUNCT_1:def 3;
y = rng (F . z) by A2, A4, FUNCT_6:def 3;
then ex x being object st
( x in dom (F . z) & a = (F . z) . x ) by A3, FUNCT_1:def 3;
hence ex x, y being object st
( x in dom F & y in dom (F . x) & a = (F . x) . y ) by A2, A4; :: thesis: verum

end;

given x, y being object such that A5: ( x in dom F & y in dom (F . x) & a = (F . x) . y ) ; :: thesis: a in Values F
(rngs F) . x = rng (F . x) by A5, FUNCT_6:def 3;
then A6: rng (F . x) in rng (rngs F) by A5, A2, FUNCT_1:def 3;
a in rng (F . x) by A5, FUNCT_1:def 3;
hence a in Values F by A6, TARSKI:def 4, A1; :: thesis: verum