let i, j be natural Number ; for D being non empty set holds (i + j) -tuples_on D = { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum }
let D be non empty set ; (i + j) -tuples_on D = { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum }
set T = { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } ;
now for x being object holds
( ( x in (i + j) -tuples_on D implies x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } ) & ( x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } implies x in (i + j) -tuples_on D ) )let x be
object ;
( ( x in (i + j) -tuples_on D implies x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } ) & ( x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,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 i,D, t is Tuple of j,D : verum } )
( x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } implies x in (i + j) -tuples_on D )proof
assume
x in (i + j) -tuples_on D
;
x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,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, Th21;
(
z is
Tuple of
i,
D &
t is
Tuple of
j,
D )
by A3, CARD_1:def 7;
hence
x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum }
by A1, A4;
verum
end; assume
x in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum }
;
x in (i + j) -tuples_on Dthen consider z being
Tuple of
i,
D,
t being
Tuple of
j,
D such that A5:
x = z ^ t
;
(
len z = i &
len t = j )
by CARD_1:def 7;
then A6:
len (z ^ t) = i + j
by FINSEQ_1:22;
z ^ t is
Element of
D *
by FINSEQ_1:def 11;
hence
x in (i + j) -tuples_on D
by A5, A6;
verum end;
hence
(i + j) -tuples_on D = { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum }
by TARSKI:2; verum