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 h be non empty homogeneous quasi_total PartFunc of (D * ),D; :: thesis: dom h = (arity h) -tuples_on D
A1: dom h c= D * by RELAT_1:def 18;
thus dom h c= (arity h) -tuples_on D :: according to XBOOLE_0:def 10 :: thesis: (arity h) -tuples_on D c= dom h

proof

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

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (arity h) -tuples_on D or x in dom h )
assume x in (arity h) -tuples_on D ; :: thesis: x in dom h
then reconsider f = x as Element of (arity h) -tuples_on D ;
consider x0 being Element of dom h;
x0 in dom h ;
then reconsider x0 = x0 as FinSequence of D by A1, FINSEQ_1:def 11;
len x0 = arity h by UNIALG_1:def 10
.= len f by FINSEQ_1:def 18 ;
hence x in dom h by UNIALG_1:def 2; :: thesis: verum