let A be non-empty with_empty-instruction UAStr ; :: thesis: dom (Den ((In (1,(dom the charact of A))),A)) = {{}}
reconsider e = the charact of A . 1 as non empty homogeneous quasi_total 0 -ary PartFunc of ( the carrier of A *), the carrier of A by Def10;
1 in dom the charact of A by Def10;
then A1: Den ((In (1,(dom the charact of A))),A) = e by SUBSET_1:def 8;
arity e = 0 by COMPUT_1:def 21;
then dom e = 0 -tuples_on the carrier of A by COMPUT_1:22;
hence dom (Den ((In (1,(dom the charact of A))),A)) = {{}} by A1, COMPUT_1:5; :: thesis: verum