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 )
thus not f is empty ; :: thesis: ( f is homogeneous & f is quasi_total )
A1: dom f = Z by FUNCOP_1:19;
thus f is homogeneous :: thesis: f is quasi_total

proof

thus dom f is with_common_domain by A1; :: according to MARGREL1:def 22 :: thesis: verum

end;

let p, q be FinSequence of X; :: according to MARGREL1:def 23 :: thesis: ( not len p = len q or not p in proj1 f or q in proj1 f )
assume that
A4: len p = len q and
A5: p in dom f ; :: thesis: q in proj1 f
len q = n by A1, A4, A5, FINSEQ_1:def 18;
then q is Element of Z by FINSEQ_2:110;
hence q in proj1 f by A1; :: thesis: verum