theorem :: CATALG_1:19

for A being non empty set
for a being Element of A holds
( the_arity_of (idsym a) = {} & the_result_sort_of (idsym a) = homsym (a,a) ) by Def3;