let D be non empty set ; :: thesis: for h being non empty homogeneous quasi_total PartFunc of (D *),D holds dom h = (arity h) -tuples_on D
let f be non empty homogeneous quasi_total PartFunc of (D *),D; :: thesis: dom f = (arity f) -tuples_on D
set y = the Element of dom f;
A1: dom f c= D * by RELAT_1:def 18;
then A2: the Element of dom f in D * ;
thus dom f c= (arity f) -tuples_on D :: according to XBOOLE_0:def 10 :: thesis: (arity f) -tuples_on D c= dom f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in (arity f) -tuples_on D )
assume A3: x in dom f ; :: thesis: x in (arity f) -tuples_on D
then reconsider x9 = x as FinSequence of D by A1, FINSEQ_1:def 11;
len x9 = arity f by A3, Def25;
then x9 is Element of (arity f) -tuples_on D by FINSEQ_2:92;
hence x in (arity f) -tuples_on D ; :: thesis: verum

end;

reconsider y = the Element of dom f as FinSequence of D by A2, FINSEQ_1:def 11;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (arity f) -tuples_on D or x in dom f )
assume x in (arity f) -tuples_on D ; :: thesis: x in dom f
then x in { s where s is Element of D * : len s = arity f } by FINSEQ_2:def 4;
then A4: ex s being Element of D * st
( x = s & len s = arity f ) ;
len y = arity f by Def25;
hence x in dom f by A4, Def22; :: thesis: verum