let i be natural Number ; :: thesis:
let D be set ; :: thesis:

reconsider j = i as Element of NAT by ORDINAL1:def 12;
let z be object ; :: thesis:
thus ( z in i -tuples_on D implies z in Funcs ((Seg i),D) ) :: thesis:

assume z in i -tuples_on D ; :: thesis:
then consider s being Element of D * such that
A1: z = s and
A2: len s = i ;
A3: rng s c= D by FINSEQ_1:def 4;
dom s = Seg i by A2, FINSEQ_1:def 3;
hence z in Funcs ((Seg i),D) by A1, A3, FUNCT_2:def 2; :: thesis:

end;

assume z in Funcs ((Seg i),D) ; :: thesis:
then consider p being Function such that
A4: z = p and
A5: dom p = Seg j and
A6: rng p c= D by FUNCT_2:def 2;
p is FinSequence by A5, FINSEQ_1:def 2;
then p is FinSequence of D by A6, FINSEQ_1:def 4;
then reconsider p = p as Element of D * by FINSEQ_1:def 11;
len p = i by A5, FINSEQ_1:def 3;
hence z in i -tuples_on D by A4; :: thesis:

end;

hence i -tuples_on D = Funcs ((Seg i),D) by TARSKI:2; :: thesis: