:: deftheorem Def3 defines with_the_same_arity COMPUT_1:def 3 :
for R being Relation holds
( R is with_the_same_arity iff for f, g being Function st f in rng R & g in rng R holds
( ( not f is empty or g is empty or dom g = {{}} ) & ( not f is empty & not g is empty implies ex n being Element of NAT ex X being non empty set st
( dom f c= n -tuples_on X & dom g c= n -tuples_on X ) ) ) );