reconsider f = the charact of A . 3 as non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of A *), the carrier of A by Def12;
3 in dom the charact of A by Def12;
then A1: Den ((In (3,(dom the charact of A))),A) = f by SUBSET_1:def 8;
arity f = 3 by COMPUT_1:def 21;
then dom f = 3 -tuples_on the carrier of A by COMPUT_1:22;
then <*C,I1,I2*> in dom f by FINSEQ_2:139;
hence (Den ((In (3,(dom the charact of A))),A)) . <*C,I1,I2*> is Algorithm of A by A1, PARTFUN1:4; :: thesis: verum