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

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