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

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 ;
( dom s = Seg i & rng s c= D ) by A2, FINSEQ_1:def 3, FINSEQ_1:def 4;
hence z in Funcs (Seg i),D by A1, FUNCT_2:def 2; :: thesis: verum

end;

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

end;

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