arity (Den ((In (3,(dom the charact of S))),S)) = 2 by ThB;
then ( dom (Den ((In (3,(dom the charact of S))),S)) = 2 -tuples_on the carrier of S & <*a,b*> is Element of 2 -tuples_on the carrier of S ) by FINSEQ_2:101, MARGREL1:22;
hence (Den ((In (3,(dom the charact of S))),S)) . <*a,b*> is Element of S by FUNCT_1:102; :: thesis: verum