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