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