let y be object ; :: thesis: for f being Function holds
( y in Union f iff ex x being object st
( x in dom f & y in f . x ) )
let f be Function; :: thesis: ( y in Union f iff ex x being object st
( x in dom f & y in f . x ) )
thus ( y in Union f implies ex x being object st
( x in dom f & y in f . x ) ) :: thesis: ( ex x being object st
( x in dom f & y in f . x ) implies y in Union f )

proof

assume y in Union f ; :: thesis: ex x being object st
( x in dom f & y in f . x )
then consider X being set such that
A1: y in X and
A2: X in rng f by TARSKI:def 4;
consider x being object such that
A3: ( x in dom f & X = f . x ) by A2, FUNCT_1:def 3;
take x ; :: thesis: ( x in dom f & y in f . x )
thus ( x in dom f & y in f . x ) by A1, A3; :: thesis: verum

end;

given x being object such that A4: x in dom f and
A5: y in f . x ; :: thesis: y in Union f
f . x in rng f by A4, FUNCT_1:def 3;
hence y in Union f by A5, TARSKI:def 4; :: thesis: verum