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)
A2: dom (X --> Y) = X by FUNCOP_1:19;
(X --> Y) . x = Y by A1, FUNCOP_1:13;
then Y in rng (X --> Y) by A1, A2, FUNCT_1:def 5;
hence Y c= Union (X --> Y) by ZFMISC_1:92; :: thesis: verum