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
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 Th125;
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 ; :: thesis: verum