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 nullary PartFunc of (the carrier of A * ),the carrier of A by Def10;
consider a being Element of A;
1 in dom the charact of A by Def10;
then A1: Den (In 1,(dom the charact of A)),A = e by FUNCT_7:def 1;
arity e = 0 by COMPUT_1:def 24;
then dom e = 0 -tuples_on the carrier of A by COMPUT_1:25;
hence dom (Den (In 1,(dom the charact of A)),A) = {{} } by A1, COMPUT_1:8; :: thesis: verum