set n = the Element of NAT ;
set y = the Element of X;
reconsider Z = the Element of NAT -tuples_on X as non empty Subset of (X *) by FINSEQ_2:90;
reconsider f = Z --> the Element of X 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 )
thus f is homogeneous ; :: thesis: f is quasi_total
let p, q be FinSequence of X; :: according to MARGREL1:def 22 :: thesis: ( not len p = len q or not p in dom f or q in dom f )
assume that
A2: len p = len q and
A3: p in dom f ; :: thesis: q in dom f
len q = the Element of NAT by A2, A3, CARD_1:def 7;
then q is Element of Z by FINSEQ_2:92;
hence q in dom f ; :: thesis: verum