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 Th23;

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 f' = f as non empty homogeneous quasi_total PartFunc of (D * ),D ;
consider x being set such that
A2: x in dom f' by XBOOLE_0:def 1;
reconsider x' = x as FinSequence of D by A2, FINSEQ_1:def 11;
A3: len x' = arity f by A2, UNIALG_1:def 10;

now

let z be set ; :: 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 z' = z as Element of (arity f) -tuples_on D ;
len z' = arity f by FINSEQ_1:def 18;
hence z in dom f by A2, A3, UNIALG_1:def 2; :: thesis: verum

end;

hence dom f = (arity f) -tuples_on D by TARSKI:2; :: 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 UNIALG_1:def 2 :: thesis: ( not len x = len y or not x in dom f or y in dom f )
assume A5: ( len x = len y & x in dom f ) ; :: thesis: y in dom f
then len x = arity f by A4, FINSEQ_1:def 18;
then y is Element of (arity f) -tuples_on D by A5, FINSEQ_2:110;
hence y in dom f by A4; :: thesis: verum

end;

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