let D be non empty set ; :: thesis:
set X = D;
let f be homogeneous PartFunc of (D *),D; :: thesis:
A1: dom f c= (arity f) -tuples_on D by Th19;

hereby :: thesis:

assume ( f is quasi_total & not f is empty ) ; :: thesis:
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;

let z be object ; :: thesis:
thus ( z in dom f implies z in (arity f) -tuples_on D ) by A1; :: thesis:
assume z in (arity f) -tuples_on D ; :: thesis:
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:

end;

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

end;

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

let x, y be FinSequence of D; :: according to MARGREL1:def 22 :: thesis:
assume that
A5: len x = len y and
A6: x in dom f ; :: thesis:
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:

end;

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