let D be non empty set ; :: thesis: for m, n being Nat holds (m + n) -tuples_on D = (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):]
let m, n be Nat; :: thesis: (m + n) -tuples_on D = (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):]
reconsider m = m, n = n as Element of NAT by ORDINAL1:def 12;
set U = D;
set LH = (m + n) -tuples_on D;
set M = m -tuples_on D;
set N = n -tuples_on D;
set C = D -concatenation ;
set RH = (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):];
B0: (m + n) -tuples_on D = { (z ^ t) where z is Tuple of m,D, t is Tuple of n,D : verum } by FINSEQ_2:105;
B1: dom (D -concatenation) = [:(D *),(D *):] by FUNCT_2:def 1;
( m -tuples_on D c= D * & n -tuples_on D c= D * ) by FINSEQ_2:134;
then B2: [:(m -tuples_on D),(n -tuples_on D):] c= [:(D *),(D *):] by ZFMISC_1:96;

now

let y be set ; :: thesis: ( y in (m + n) -tuples_on D implies y in (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] )
assume y in (m + n) -tuples_on D ; :: thesis: y in (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):]
then consider Tz being Tuple of m,D, Tt being Tuple of n,D such that
C0: y = Tz ^ Tt by B0;
reconsider zz = Tz as Element of m -tuples_on D by FINSEQ_2:131;
reconsider tt = Tt as Element of n -tuples_on D by FINSEQ_2:131;
reconsider x = [zz,tt] as Element of [:(m -tuples_on D),(n -tuples_on D):] ;
reconsider xx = x as Element of dom (D -concatenation) by B1, B2, TARSKI:def 3;
C1: (D -concatenation) .: {x} c= (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] by RELAT_1:123;
y = (D -concatenation) . (Tz,Tt) by C0, ThConcatenation
.= (D -concatenation) . x ;
then y in {((D -concatenation) . xx)} by TARSKI:def 1;
then y in Im ((D -concatenation),xx) by FUNCT_1:59;
hence y in (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] by C1; :: thesis: verum

end;

then B3: (m + n) -tuples_on D c= (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] by TARSKI:def 3;

now

let y be set ; :: thesis: ( y in (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] implies y in (m + n) -tuples_on D )
assume y in (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] ; :: thesis: y in (m + n) -tuples_on D
then consider x being set such that
C0: ( x in dom (D -concatenation) & x in [:(m -tuples_on D),(n -tuples_on D):] & y = (D -concatenation) . x ) by FUNCT_1:def 6;
consider z, t being set such that
C1: ( z in m -tuples_on D & t in n -tuples_on D & x = [z,t] ) by C0, ZFMISC_1:def 2;
reconsider zz = z as Element of m -tuples_on D by C1;
reconsider tt = t as Element of n -tuples_on D by C1;
reconsider zzz = zz, ttt = tt as FinSequence of D ;
reconsider Tz = zz as Tuple of m,D ;
reconsider Tt = tt as Tuple of n,D ;
y = (D -concatenation) . (zzz,ttt) by C0, C1
.= Tz ^ Tt by ThConcatenation ;
hence y in (m + n) -tuples_on D by B0; :: thesis: verum

end;

then (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] c= (m + n) -tuples_on D by TARSKI:def 3;
hence (m + n) -tuples_on D = (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] by B3, XBOOLE_0:def 10; :: thesis: verum