let X, Y be set ; :: thesis: ( X <> {} implies Union (X --> Y) = Y )
assume A1: X <> {} ; :: thesis: Union (X --> Y) = Y
set x = the Element of X;
thus Union (X --> Y) c= Y by Th6; :: according to XBOOLE_0:def 10 :: thesis: Y c= Union (X --> Y)
A2: dom (X --> Y) = X ;
(X --> Y) . the Element of X = Y by A1, FUNCOP_1:7;
then Y in rng (X --> Y) by A1, A2, FUNCT_1:def 3;
hence Y c= Union (X --> Y) by ZFMISC_1:74; :: thesis: verum