let i be Nat; :: thesis: for D being non empty set holds i -tuples_on D = Funcs (Seg i),D
let D be non empty set ; :: thesis: i -tuples_on D = Funcs (Seg i),D

now

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

proof

assume z in i -tuples_on D ; :: thesis: z in Funcs (Seg i),D
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: verum

end;

assume z in Funcs (Seg i),D ; :: thesis: z in i -tuples_on D
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: verum

end;

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