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

end;

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 consider s being Element of D * such that
A3: ( x = s & len s = arity f ) ;
A4: dom f <> {} by UNIALG_1:1;
consider y being Element of dom f;
y in D * by A1, A4, TARSKI:def 3;
then reconsider y = y as FinSequence of D by FINSEQ_1:def 11;
len y = arity f by A4, UNIALG_1:def 10;
hence x in dom f by A3, A4, UNIALG_1:def 2; :: thesis: verum