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):];
A1: (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;
A2: dom (D -concatenation) = [:(D *),(D *):] by FUNCT_2:def 1;
A3: ( m -tuples_on D c= D * & n -tuples_on D c= D * ) by FINSEQ_2:134;

now :: thesis: for y being object st y in (m + n) -tuples_on D holds
y in (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):]

let y be object ; :: 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
A4: y = Tz ^ Tt by A1;
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 A2, A3, ZFMISC_1:96, TARSKI:def 3;
A5: (D -concatenation) .: {x} c= (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] by RELAT_1:123;
y = (D -concatenation) . (Tz,Tt) by A4, Lm10
.= (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 A5; :: thesis: verum

end;

then A6: (m + n) -tuples_on D c= (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] ;

now :: thesis: for y being object st y in (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] holds
y in (m + n) -tuples_on D

let y be object ; :: 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 object such that
A7: ( 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 object such that
A8: ( z in m -tuples_on D & t in n -tuples_on D & x = [z,t] ) by ZFMISC_1:def 2, A7;
reconsider zz = z as Element of m -tuples_on D by A8;
reconsider tt = t as Element of n -tuples_on D by A8;
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 A7, A8
.= Tz ^ Tt by Lm10 ;
hence y in (m + n) -tuples_on D by A1; :: thesis: verum

end;

then (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] c= (m + n) -tuples_on D ;
hence (m + n) -tuples_on D = (D -concatenation) .: [:(m -tuples_on D),(n -tuples_on D):] by A6; :: thesis: verum