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

now

let x be set ; :: thesis: ( ( x in (i + j) -tuples_on D implies x in { (z ^ t) where z is Tuple of ,D, t is Tuple of ,D : verum } ) & ( x in { (z ^ t) where z is Tuple of ,D, t is Tuple of ,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 Tuple of ,D, t is Tuple of ,D : verum } ) :: thesis: ( x in { (z ^ t) where z is Tuple of ,D, t is Tuple of ,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 Tuple of ,D, t is Tuple of ,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 Tuple of ,D & t is Tuple of ,D ) by A3, FINSEQ_1:def 18;
hence x in { (z ^ t) where z is Tuple of ,D, t is Tuple of ,D : verum } by A1, A4; :: thesis: verum

end;

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

end;

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