let i, j be Nat; :: thesis: for D being non empty set holds (i + j) -tuples_on D = { (z ^ t) where z is Element of i -tuples_on D, t is Element of j -tuples_on D : verum }
let D be non empty set ; :: thesis: (i + j) -tuples_on D = { (z ^ t) where z is Element of i -tuples_on D, t is Element of j -tuples_on D : verum }
set T = { (z ^ t) where z is Element of i -tuples_on D, t is Element of j -tuples_on D : verum } ;

now

let x be set ; :: thesis: ( ( x in (i + j) -tuples_on D implies x in { (z ^ t) where z is Element of i -tuples_on D, t is Element of j -tuples_on D : verum } ) & ( x in { (z ^ t) where z is Element of i -tuples_on D, t is Element of j -tuples_on D : verum } implies x in (i + j) -tuples_on D ) )
thus ( x in (i + j) -tuples_on D implies x in { (z ^ t) where z is Element of i -tuples_on D, t is Element of j -tuples_on D : verum } ) :: thesis: ( x in { (z ^ t) where z is Element of i -tuples_on D, t is Element of j -tuples_on D : verum } implies x in (i + j) -tuples_on D )

proof

assume x in (i + j) -tuples_on D ; :: thesis: x in { (z ^ t) where z is Element of i -tuples_on D, t is Element of j -tuples_on D : verum }
then consider s being Element of D * such that
A1: x = s and
A2: len s = i + j ;
consider z, t being FinSequence of D such that
A3: ( len z = i & len t = j ) and
A4: s = z ^ t by A2, Th26;
( z is Element of i -tuples_on D & t is Element of j -tuples_on D ) by A3, Th110;
hence x in { (z ^ t) where z is Element of i -tuples_on D, t is Element of j -tuples_on D : verum } by A1, A4; :: thesis: verum

end;

assume x in { (z ^ t) where z is Element of i -tuples_on D, t is Element of j -tuples_on D : verum } ; :: thesis: x in (i + j) -tuples_on D
then consider z being Element of i -tuples_on D, t being Element of j -tuples_on D such that
A5: x = z ^ t ;
( len z = i & len t = j & z ^ t in D * ) by FINSEQ_1:def 11, FINSEQ_1:def 18;
then ( len (z ^ t) = i + j & z ^ t is Element of D * ) by FINSEQ_1:35;
hence x in (i + j) -tuples_on D by A5; :: thesis: verum

end;

hence (i + j) -tuples_on D = { (z ^ t) where z is Element of i -tuples_on D, t is Element of j -tuples_on D : verum } by TARSKI:2; :: thesis: verum