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:8;
then union (rng (X --> Y)) = Y by ZFMISC_1:25;
hence ( Union (X --> Y) = Y & meet (X --> Y) = Y ) by A1, CARD_3:def 4, SETFAM_1:10; :: thesis: verum