let i, j be natural Number ; for D being non empty set
for s being Tuple of i + j,D ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t
let D be non empty set ; for s being Tuple of i + j,D ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t
let s be Tuple of i + j,D; ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t
A1:
s is Element of D *
by FINSEQ_1:def 11;
len s = i + j
by CARD_1:def 7;
then
s in (i + j) -tuples_on D
by A1;
then
s in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum }
by Th103;
then consider z being Tuple of i,D, t being Tuple of j,D such that
A2:
s = z ^ t
;
reconsider z = z as Element of i -tuples_on D by Lm6;
reconsider t = t as Element of j -tuples_on D by Lm6;
s = z ^ t
by A2;
hence
ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t
; verum