set F = Den o,U0;
set S0 = the Sorts of U0;
set RS = the ResultSort of S;
set rs = the_result_sort_of o;
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 5, 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