let i, j be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t
A: s is Element of D * by FINSEQ_1:def 11;
len s = i + j by FINSEQ_1:def 18;
then s in (i + j) -tuples_on D by A;
then s in { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum } by Th125;
then consider z being Tuple of i,D, t being Tuple of j,D such that
W: s = z ^ t ;
reconsider z = z as Element of i -tuples_on D by Lemat;
reconsider t = t as Element of j -tuples_on D by Lemat;
s = z ^ t by W;
hence ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t ; :: thesis: verum