let X, Y be set ; :: thesis: ( X <> {} implies ( Union (X --> Y) = Y & meet (X --> Y) = Y ) )
assume X <> {} ; :: thesis: ( Union (X --> Y) = Y & meet (X --> Y) = Y )
then A1: rng (X --> Y) = {Y} by FUNCOP_1:14;
then union (rng (X --> Y)) = Y by ZFMISC_1:31;
hence ( Union (X --> Y) = Y & meet (X --> Y) = Y ) by A1, CARD_3:def 4, SETFAM_1:11; :: thesis: verum