theorem :: CATALG_1:20

for A being non empty set
for a, b, c being Element of A holds
( the_arity_of (compsym (a,b,c)) = <*(homsym (b,c)),(homsym (a,b))*> & the_result_sort_of (compsym (a,b,c)) = homsym (a,c) ) by Def3;