set F = Den (o,U0);
set S0 = the Sorts of U0;
dom (Den (o,U0)) = Args (o,U0)
by FUNCT_2:def 1;
then
( rng (Den (o,U0)) c= Result (o,U0) & (Den (o,U0)) . p in rng (Den (o,U0)) )
by A1, FUNCT_1:def 3, RELAT_1:def 19;
then
(Den (o,U0)) . p in union (rng the Sorts of U0)
by TARSKI:def 4;
hence
(Den (o,U0)) . p is Element of Union the Sorts of U0
by CARD_3:def 4; verum