let X, Y be set ; :: thesis: ( X <> {} implies Union (X --> Y) = Y )
assume A1: X <> {} ; :: thesis: Union (X --> Y) = Y
consider x being Element of X;
thus Union (X --> Y) c= Y by Th15; :: according to XBOOLE_0:def 10 :: thesis: Y c= Union (X --> Y)
( dom (X --> Y) = X & (X --> Y) . x = Y ) by A1, FUNCOP_1:13, FUNCOP_1:19;
then ( Y in rng (X --> Y) & Union (X --> Y) = union (rng (X --> Y)) ) by A1, FUNCT_1:def 5;
hence Y c= Union (X --> Y) by ZFMISC_1:92; :: thesis: verum