let F be 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 ) )
let a be object ; ( 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 ) )
( ex x, y being object st
( x in dom F & y in dom (F . x) & a = (F . x) . y ) implies a in Values F )
given x, y being object such that A5:
( x in dom F & y in dom (F . x) & a = (F . x) . y )
; 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; verum