let f be NAT * -defined homogeneous Function; :: thesis: dom f c= (arity f) -tuples_on NAT
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in (arity f) -tuples_on NAT )
assume A1: x in dom f ; :: thesis: x in (arity f) -tuples_on NAT
reconsider x9 = x as FinSequence of NAT by A1, FINSEQ_1:def 11;
len x9 = arity f by A1, MARGREL1:def 25;
then x9 is Element of (arity f) -tuples_on NAT by FINSEQ_2:92;
hence x in (arity f) -tuples_on NAT ; :: thesis: verum