let D be non empty set ; :: thesis: for f being homogeneous PartFunc of (D *),D holds
( ( f is quasi_total & not f is empty ) iff dom f = (arity f) -tuples_on D )
set X = D;
let f be homogeneous PartFunc of (D *),D; :: thesis: ( ( f is quasi_total & not f is empty ) iff dom f = (arity f) -tuples_on D )
A1: dom f c= (arity f) -tuples_on D by Th19;

hereby :: thesis: ( dom f = (arity f) -tuples_on D implies ( f is quasi_total & not f is empty ) )

assume ( f is quasi_total & not f is empty ) ; :: thesis: dom f = (arity f) -tuples_on D
then reconsider f9 = f as non empty homogeneous quasi_total PartFunc of (D *),D ;
consider x being object such that
A2: x in dom f9 by XBOOLE_0:def 1;
reconsider x9 = x as FinSequence of D by A2, FINSEQ_1:def 11;
A3: len x9 = arity f by A2, MARGREL1:def 25;

now :: thesis: for z being object holds
( ( z in dom f implies z in (arity f) -tuples_on D ) & ( z in (arity f) -tuples_on D implies z in dom f ) )

let z be object ; :: thesis: ( ( z in dom f implies z in (arity f) -tuples_on D ) & ( z in (arity f) -tuples_on D implies z in dom f ) )
thus ( z in dom f implies z in (arity f) -tuples_on D ) by A1; :: thesis: ( z in (arity f) -tuples_on D implies z in dom f )
assume z in (arity f) -tuples_on D ; :: thesis: z in dom f
then reconsider z9 = z as Element of (arity f) -tuples_on D ;
len z9 = arity f by CARD_1:def 7;
hence z in dom f by A2, A3, MARGREL1:def 22; :: thesis: verum

end;

hence dom f = (arity f) -tuples_on D ; :: thesis: verum

end;

assume A4: dom f = (arity f) -tuples_on D ; :: thesis: ( f is quasi_total & not f is empty )
thus f is quasi_total :: thesis: not f is empty

proof

let x, y be FinSequence of D; :: according to MARGREL1:def 22 :: thesis: ( not len x = len y or not x in dom f or y in dom f )
assume that
A5: len x = len y and
A6: x in dom f ; :: thesis: y in dom f
len x = arity f by A4, A6, CARD_1:def 7;
then y is Element of (arity f) -tuples_on D by A5, FINSEQ_2:92;
hence y in dom f by A4; :: thesis: verum

end;

thus not f is empty by A4; :: thesis: verum