let i be natural Number ; :: thesis: for D being set holds i -tuples_on D = Funcs ((Seg i),D)
let D be set ; :: thesis: i -tuples_on D = Funcs ((Seg i),D)

now :: thesis: for z being object holds
( ( 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 ) )

reconsider j = i as Element of NAT by ORDINAL1:def 12;
let z be object ; :: 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