:: deftheorem defines equal-arity PRALG_1:def 18 :
for IT being Function holds
( IT is equal-arity iff for x, y being set st x in dom IT & y in dom IT holds
for f, g being Function st IT . x = f & IT . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of (X *),X
for o2 being non empty homogeneous quasi_total PartFunc of (Y *),Y st f = o1 & g = o2 holds
arity o1 = arity o2 );