let A be set ; :: thesis: for D being non empty set
for m being Nat st A is D -prefix holds
(D -multiCat) .: (m -tuples_on A) is D -prefix
let D be non empty 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 A2: (D -multiCat) .: (m -tuples_on A) = (D -multiCat) .: {(<*> A)} by FINSEQ_2:94
.= Im ((D -multiCat),{})
.= {((D -multiCat) . {})} by FUNCT_1:59, A1
.= {{}} ;
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 A3: ( 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 A4: ( x = {} & y = {} ) by TARSKI:def 1, A2;
reconsider xx = x as Element of D * by A3;
reconsider yy = y as Element of D * by A3;
reconsider d11 = d1 as Element of D * by A3;
reconsider d22 = d2 as Element of D * by A3;
d11 = xx ^ d11 by A4, FINSEQ_1:34
.= f . (yy,d22) by Lm10, A3
.= {} ^ d22 by A4, Lm10
.= d22 by FINSEQ_1:34 ;
hence ( x = y & d1 = d2 ) by A4; :: thesis: verum
end;
hence ( A is D -prefix implies (D -multiCat) .: (m -tuples_on A) is D -prefix ) by Def10; :: 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
A5: 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 Lm5;
then (k + 1) -tuples_on A misses {{}} by Lm6;
then A6: ((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 A7: (MultPlace f) .: ((k + 1) -tuples_on A) is f -unambiguous by Lm19;
(D -multiCat) .: ((k + 1) -tuples_on A) = ((D -multiCat) | (((k + 1) -tuples_on A) \ {{}})) .: (((k + 1) -tuples_on A) \ {{}}) by RELAT_1:129, A6
.= ((MultPlace f) | ((k + 1) -tuples_on A)) .: ((k + 1) -tuples_on A) by A6, Lm24
.= (MultPlace f) .: ((k + 1) -tuples_on A) by RELAT_1:129 ;
hence (D -multiCat) .: (m -tuples_on A) is D -prefix by A5, A7; :: thesis: verum
end;
end;