reconsider f = the charact of A . 2 as non empty homogeneous quasi_total binary PartFunc of (the carrier of A * ),the carrier of A by Def11;
2 in dom the charact of A by Def11;
then A1: Den (In 2,(dom the charact of A)),A = f by FUNCT_7:def 1;
then dom f = 2 -tuples_on the carrier of A by Th44;
then <*I1,I2*> in dom f by CATALG_1:10;
hence (Den (In 2,(dom the charact of A)),A) . <*I1,I2*> is Algorithm of A by A1, PARTFUN1:27; :: thesis: verum