arity (Den ((In (1,(dom the charact of S))),S)) = 0 by ThB;
then dom (Den ((In (1,(dom the charact of S))),S)) = 0 -tuples_on the carrier of S by COMPUT_1:22
.= {{}} by COMPUT_1:5 ;
then {} in dom (Den ((In (1,(dom the charact of S))),S)) by TARSKI:def 1;
hence (Den ((In (1,(dom the charact of S))),S)) . {} is Element of S by FUNCT_1:102; :: thesis: verum