assume not Union f is empty ; :: thesis: contradiction
then consider y being object such that
A1: y in Union f by XBOOLE_0:def 1;
y in union (rng f) by A1, CARD_3:def 4;
then consider Y being set such that
A2: ( y in Y & Y in rng f ) by TARSKI:def 4;
thus contradiction by A2; :: thesis: verum