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
A1: dom f <> {} by RELAT_1:64;
consider y being Element of dom f;
A2: dom f c= D * by RELAT_1:def 18;
then A3: y in D * by A1, TARSKI:def 3;
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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in (arity f) -tuples_on D )
assume A4: x in dom f ; :: thesis: x in (arity f) -tuples_on D
then reconsider x9 = x as FinSequence of D by A2, FINSEQ_1:def 11;
len x9 = arity f by A4, UNIALG_1:def 10;
then x9 is Element of (arity f) -tuples_on D by FINSEQ_2:110;
hence x in (arity f) -tuples_on D ; :: thesis: verum

end;

reconsider y = y as FinSequence of D by A3, FINSEQ_1:def 11;
let x be set ; :: 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 A5: ex s being Element of D * st
( x = s & len s = arity f ) ;
len y = arity f by A1, UNIALG_1:def 10;
hence x in dom f by A5, A1, UNIALG_1:def 2; :: thesis: verum