reconsider f = the charact of A . 4 as non empty homogeneous quasi_total binary PartFunc of ( the carrier of A *), the carrier of A by Def13;
4 in dom the charact of A by Def13;
then A1: Den ((In (4,(dom the charact of A))),A) = f by FUNCT_7:def 1;
arity f = 2 by COMPUT_1:def 26;
then dom f = 2 -tuples_on the carrier of A by COMPUT_1:25;
then <*C,I*> in dom f by FINSEQ_2:157;
hence (Den ((In (4,(dom the charact of A))),A)) . <*C,I*> is Algorithm of A by A1, PARTFUN1:27; :: thesis: verum