let A be set ; :: thesis: for D being non empty set
for m being Nat st A is D -prefix holds
D -multiCat is m -tuples_on A -one-to-one
let D be non empty 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 A1: A is D -prefix ; :: thesis: D -multiCat is m -tuples_on A -one-to-one
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 Lm7
.= {{}} 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 ; :: thesis: verum
end;
suppose m <> 0 ; :: thesis: D -multiCat is m -tuples_on A -one-to-one
then consider k being Nat such that
A2: 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 A1, Lm21;
then A3: (MultPlace (D -concatenation)) | (kk -tuples_on A) is one-to-one ;
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 Lm24, A3, A2;
hence D -multiCat is m -tuples_on A -one-to-one ; :: thesis: verum
end;
end;