let f be NAT * -defined homogeneous Function; :: thesis: dom f c= (arity f) -tuples_on NAT
let x be set ; :: 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
dom f c= NAT * by RELAT_1:def 18;
then reconsider x' = x as FinSequence of NAT by A1, FINSEQ_1:def 11;
len x' = arity f by A1, UNIALG_1:def 10;
then x' is Element of (arity f) -tuples_on NAT by FINSEQ_2:110;
hence x in (arity f) -tuples_on NAT ; :: thesis: verum