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;
then dom e = {{}} by Th42;
then {} in dom e by TARSKI:def 1;
hence (Den ((In (1,(dom the charact of A))),A)) . {} is Algorithm of A by A1, PARTFUN1:4; :: thesis: verum