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;
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;
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:27; :: thesis: verum