reconsider f = the charact of A . 3 as non empty homogeneous quasi_total ternary PartFunc of (the carrier of A * ),the carrier of A by Def12;
( 3 in dom the charact of A & 3 in Seg 3 ) by Def12;
then A1: Den (In 3,(dom the charact of A)),A = f by FUNCT_7:def 1;
arity f = 3 by COMPUT_1:def 27;
then dom f = 3 -tuples_on the carrier of A by COMPUT_1:25;
then <*C,I1,I2*> in dom f by CATALG_1:12;
hence (Den (In 3,(dom the charact of A)),A) . <*C,I1,I2*> is Algorithm of A by A1, PARTFUN1:27; :: thesis: verum