consider n being Element of NAT , y being Element of X;
reconsider Z = n -tuples_on X as non empty Subset of (X * ) by Th13;
reconsider f = Z --> y as PartFunc of (X * ),X ;
take f ; :: thesis: ( not f is empty & f is homogeneous & f is quasi_total )
A1: dom f = Z by FUNCOP_1:19;
thus not f is empty ; :: thesis: ( f is homogeneous & f is quasi_total )
thus f is homogeneous :: thesis: f is quasi_total

proof

let x, y be FinSequence; :: according to UNIALG_1:def 1 :: thesis: ( not x in dom f or not y in dom f or len x = len y )
assume ( x in dom f & y in dom f ) ; :: thesis: len x = len y
then ( len x = n & len y = n ) by A1, FINSEQ_1:def 18;
hence len x = len y ; :: thesis: verum

end;

let p, q be FinSequence of X; :: according to UNIALG_1:def 2 :: thesis: ( not len p = len q or not p in dom f or q in dom f )
assume ( len p = len q & p in dom f ) ; :: thesis: q in dom f
then len q = n by A1, FINSEQ_1:def 18;
then q is Element of Z by FINSEQ_2:110;
hence q in dom f by A1; :: thesis: verum