let D be non empty set ; :: thesis: for f being non empty homogeneous PartFunc of (D * ),D
for n being Element of NAT st dom f c= n -tuples_on D holds
arity f = n
let f be non empty homogeneous PartFunc of (D * ),D; :: thesis: for n being Element of NAT st dom f c= n -tuples_on D holds
arity f = n
let n be Element of NAT ; :: thesis: ( dom f c= n -tuples_on D implies arity f = n )
assume A1: dom f c= n -tuples_on D ; :: thesis: arity f = n
consider x being set such that
A2: x in dom f by XBOOLE_0:def 1;
reconsider x = x as Element of n -tuples_on D by A1, A2;
A3: x in dom f by A2;
for x being FinSequence st x in dom f holds
n = len x by A1, FINSEQ_1:def 18;
hence arity f = n by A3, UNIALG_1:def 10; :: thesis: verum