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 rng (X --> Y) = {Y} by FUNCOP_1:14;
then ( union (rng (X --> Y)) = Y & meet (rng (X --> Y)) = Y ) by SETFAM_1:11, ZFMISC_1:31;
hence ( Union (X --> Y) = Y & meet (X --> Y) = Y ) by CARD_3:def 4; :: thesis: verum