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

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