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
set x0 = the Element of dom h;
A1: the Element of dom h in dom h ;
A2: dom h c= D * by RELAT_1:def 18;
then reconsider x0 = the Element of dom h as FinSequence of D by A1, FINSEQ_1:def 11;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom h or x in (arity h) -tuples_on D )
assume A3: x in dom h ; :: thesis: x in (arity h) -tuples_on D
then reconsider f = x as FinSequence of D by A2, FINSEQ_1:def 11;
A4: f is Element of (len f) -tuples_on D by FINSEQ_2:92;
len f = arity h by A3, MARGREL1:def 25;
hence x in (arity h) -tuples_on D by A4; :: thesis: verum
end;
let x be object ; :: 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 ;
len x0 = arity h by MARGREL1:def 25
.= len f by CARD_1:def 7 ;
hence x in dom h by MARGREL1:def 22; :: thesis: verum