let X be non empty set ; :: thesis: for x being Element of X
for n being Nat holds arity ((n -tuples_on X) --> x) = n
let x be Element of X; :: thesis: for n being Nat holds arity ((n -tuples_on X) --> x) = n
let n be Nat; :: thesis: arity ((n -tuples_on X) --> x) = n
reconsider m = n as Element of NAT by ORDINAL1:def 12;
set f = (n -tuples_on X) --> x;
dom ((n -tuples_on X) --> x) = m -tuples_on X by FUNCOP_1:13;
hence arity ((n -tuples_on X) --> x) = n by COMPUT_1:24; :: thesis: verum