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

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