let D be non empty set ; :: thesis: for A being set
for m being Nat st A is D -prefix holds
D -multiCat is m -tuples_on A -one-to-one
let A be set ; :: thesis: for m being Nat st A is D -prefix holds
D -multiCat is m -tuples_on A -one-to-one
let m be Nat; :: thesis: ( A is D -prefix implies D -multiCat is m -tuples_on A -one-to-one )
set f = D -concatenation ;
set F = D -multiCat ;
set Z = m -tuples_on A;
assume A is D -prefix ; :: thesis: D -multiCat is m -tuples_on A -one-to-one
then B1: ( D -concatenation is associative & A is D -concatenation -unambiguous ) by DefPrefix;

per cases ( m = 0 or m <> 0 ) ;

suppose m = 0 ; :: thesis: D -multiCat is m -tuples_on A -one-to-one

then m -tuples_on A = Funcs ((Seg 0),A) by Lm21
.= {{}} by FUNCT_5:57 ;
then (D -multiCat) | (m -tuples_on A) is one-to-one ;
hence D -multiCat is m -tuples_on A -one-to-one by DefInj1; :: thesis: verum

end;

suppose m <> 0 ; :: thesis: D -multiCat is m -tuples_on A -one-to-one

then consider k being Nat such that
C1: m = k + 1 by NAT_1:6;
reconsider kk = k + 1 as Element of NAT by ORDINAL1:def 12;
set ZZ = kk -tuples_on A;
MultPlace (D -concatenation) is kk -tuples_on A -one-to-one by B1, Lm26;
then C2: (MultPlace (D -concatenation)) | (kk -tuples_on A) is one-to-one by DefInj1;
len {} = 0 ;
then not {} in kk -tuples_on A by FINSEQ_2:132;
then {{}} misses kk -tuples_on A by ZFMISC_1:50;
then (kk -tuples_on A) \ {{}} = kk -tuples_on A by XBOOLE_1:83;
then (D -multiCat) | (m -tuples_on A) is one-to-one by Lm16, C2, C1;
hence D -multiCat is m -tuples_on A -one-to-one by DefInj1; :: thesis: verum

end;

end;