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 A1: ( 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 FINSEQ_2:142, TARSKI:def 3;
reconsider xx1 = x1111, xx2 = x2222, dd1 = d1, dd2 = d2 as FinSequence of D by FINSEQ_1:def 11, A1;
( len xx1 = 1 & len xx2 = 1 ) by CARD_1:def 7;
then A2: ( xx1 = <*(xx1 . 1)*> & xx2 = <*(xx2 . 1)*> ) by FINSEQ_1:40;
A3: ( (D -concatenation) . (x1,d1) = xx1 ^ dd1 & (D -concatenation) . (x2,d2) = xx2 ^ dd2 ) by Lm10;
assume A4: (D -concatenation) . (x1,d1) = (D -concatenation) . (x2,d2) ; :: thesis: ( x1 = x2 & d1 = d2 )
A5: xx1 . 1 = (xx1 ^ dd1) . 1 by A2, FINSEQ_1:41
.= xx2 . 1 by A2, A4, A3, FINSEQ_1:41 ;
thus ( x1 = x2 & d1 = d2 ) by FINSEQ_1:33, A5, A2, A4, A3; :: thesis: verum