set f = D -concatenation ;
set D1 = 1 -tuples_on D;
let X be Subset of (1 -tuples_on D); :: thesis: X is D -prefix
B1: 1 -tuples_on D c= D * by FINSEQ_2:134;

now

let x1, x2, d1, d2 be set ; :: thesis: ( x1 in X /\ (D *) & x2 in X /\ (D *) & d1 in D * & d2 in D * & (D -concatenation) . (x1,d1) = (D -concatenation) . (x2,d2) implies ( x1 = x2 & d1 = d2 ) )
assume C1: ( x1 in X /\ (D *) & x2 in X /\ (D *) & d1 in D * & d2 in D * ) ; :: thesis: ( (D -concatenation) . (x1,d1) = (D -concatenation) . (x2,d2) implies ( x1 = x2 & d1 = d2 ) )
then reconsider x11 = x1, x22 = x2 as Element of 1 -tuples_on D ;
reconsider x111 = x11, x222 = x22 as 1 -element FinSequence ;
reconsider x1111 = x11, x2222 = x22 as Element of D * by B1, TARSKI:def 3;
reconsider xx1 = x1111, xx2 = x2222, dd1 = d1, dd2 = d2 as FinSequence of D by C1, FINSEQ_1:def 11;
( len xx1 = 1 & len xx2 = 1 ) by CARD_1:def 7;
then C3: ( xx1 = <*(xx1 . 1)*> & xx2 = <*(xx2 . 1)*> ) by FINSEQ_1:40;
C2: ( (D -concatenation) . (x1,d1) = xx1 ^ dd1 & (D -concatenation) . (x2,d2) = xx2 ^ dd2 ) by ThConcatenation;
assume Z1: (D -concatenation) . (x1,d1) = (D -concatenation) . (x2,d2) ; :: thesis: ( x1 = x2 & d1 = d2 )
Z2: xx1 . 1 = (xx1 ^ dd1) . 1 by C3, FINSEQ_1:41
.= xx2 . 1 by C3, Z1, C2, FINSEQ_1:41 ;
thus ( x1 = x2 & d1 = d2 ) by Z2, C3, Z1, C2, FINSEQ_1:33; :: thesis: verum

end;

then X is D -concatenation -unambiguous by DefUnambiguous2;
hence X is D -prefix by DefPrefix; :: thesis: verum