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; :: thesis: verum