let D be non empty set ; :: thesis: for f being non empty homogeneous PartFunc of (D *),D
for n being 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 Nat st dom f c= n -tuples_on D holds
arity f = n
let n be Nat; :: thesis: ( dom f c= n -tuples_on D implies arity f = n )
consider x being object such that
A1: x in dom f by XBOOLE_0:def 1;
assume A2: dom f c= n -tuples_on D ; :: thesis: arity f = n
then A3: for x being FinSequence st x in dom f holds
n = len x by CARD_1:def 7;
reconsider x = x as Element of n -tuples_on D by A2, A1;
x in dom f by A1;
hence arity f = n by A3, MARGREL1:def 25; :: thesis: verum