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