let D be non empty set ; :: thesis: for A being set
for m being Nat st A is D -prefix holds
(D -multiCat) .: (m -tuples_on A) is D -prefix
let A be set ; :: thesis: for m being Nat st A is D -prefix holds
(D -multiCat) .: (m -tuples_on A) is D -prefix
let m be Nat; :: thesis: ( A is D -prefix implies (D -multiCat) .: (m -tuples_on A) is D -prefix )
reconsider f = D -concatenation as BinOp of (D *) ;
set F = D -multiCat ;
set Y = (D -multiCat) .: (m -tuples_on A);
{} in (D *) * by FINSEQ_1:49;
then A1: {} in dom (D -multiCat) by FUNCT_2:def 1;

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

suppose m = 0 ; :: thesis: ( A is D -prefix implies (D -multiCat) .: (m -tuples_on A) is D -prefix )

then Z1: (D -multiCat) .: (m -tuples_on A) = (D -multiCat) .: {(<*> A)} by FINSEQ_2:94
.= Im ((D -multiCat),{})
.= {((D -multiCat) . {})} by A1, FUNCT_1:59
.= {{}} ;
for x, y, d1, d2 being set st x in ((D -multiCat) .: (m -tuples_on A)) /\ (D *) & y in ((D -multiCat) .: (m -tuples_on A)) /\ (D *) & d1 in D * & d2 in D * & f . (x,d1) = f . (y,d2) holds
( x = y & d1 = d2 )

proof

let x, y, d1, d2 be set ; :: thesis: ( x in ((D -multiCat) .: (m -tuples_on A)) /\ (D *) & y in ((D -multiCat) .: (m -tuples_on A)) /\ (D *) & d1 in D * & d2 in D * & f . (x,d1) = f . (y,d2) implies ( x = y & d1 = d2 ) )
assume C1: ( x in ((D -multiCat) .: (m -tuples_on A)) /\ (D *) & y in ((D -multiCat) .: (m -tuples_on A)) /\ (D *) & d1 in D * & d2 in D * & f . (x,d1) = f . (y,d2) ) ; :: thesis: ( x = y & d1 = d2 )
then ( x in (D -multiCat) .: (m -tuples_on A) & x in D * & y in (D -multiCat) .: (m -tuples_on A) & y in D * ) by XBOOLE_0:def 4;
then C3: ( x = {} & y = {} ) by Z1, TARSKI:def 1;
reconsider xx = x as Element of D * by C1;
reconsider yy = y as Element of D * by C1;
reconsider d11 = d1 as Element of D * by C1;
reconsider d22 = d2 as Element of D * by C1;
d11 = xx ^ d11 by C3, FINSEQ_1:34
.= f . (yy,d22) by ThConcatenation, C1
.= {} ^ d22 by C3, ThConcatenation
.= d22 by FINSEQ_1:34 ;
hence ( x = y & d1 = d2 ) by C3; :: thesis: verum

end;

then (D -multiCat) .: (m -tuples_on A) is f -unambiguous by DefUnambiguous2;
hence ( A is D -prefix implies (D -multiCat) .: (m -tuples_on A) is D -prefix ) by DefPrefix; :: thesis: verum

end;

suppose m <> 0 ; :: thesis: ( A is D -prefix implies (D -multiCat) .: (m -tuples_on A) is D -prefix )

then consider k being Nat such that
C0: m = k + 1 by NAT_1:6;
set B = (k + 1) -tuples_on A;
(k + 1) -tuples_on A misses 0 -tuples_on A by Lm18;
then (k + 1) -tuples_on A misses {{}} by COMPUT_1:5;
then C1: ((k + 1) -tuples_on A) \ {{}} = (k + 1) -tuples_on A by XBOOLE_1:83;
assume A is D -prefix ; :: thesis: (D -multiCat) .: (m -tuples_on A) is D -prefix
then A is f -unambiguous by DefPrefix;
then C2: (MultPlace f) .: ((k + 1) -tuples_on A) is f -unambiguous by Lm15;
(D -multiCat) .: ((k + 1) -tuples_on A) = ((D -multiCat) | (((k + 1) -tuples_on A) \ {{}})) .: (((k + 1) -tuples_on A) \ {{}}) by C1, RELAT_1:129
.= ((MultPlace f) | ((k + 1) -tuples_on A)) .: ((k + 1) -tuples_on A) by C1, Lm16
.= (MultPlace f) .: ((k + 1) -tuples_on A) by RELAT_1:129 ;
hence (D -multiCat) .: (m -tuples_on A) is D -prefix by C0, C2, DefPrefix; :: thesis: verum

end;

end;