set f = U -concatenation ;
set D = U * ;
defpred S₁[ set ] means $1 is FinSequence of U;
defpred S₂[] means for p1, q1, p2, q2 being U -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds
( p1 = p2 & q1 = q2 );
thus ( X is U -prefix implies S₂[] ) :: thesis: ( ( for p1, q1, p2, q2 being U -valued FinSequence st p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 holds
( p1 = p2 & q1 = q2 ) ) implies X is U -prefix )

proof

assume X is U -prefix ; :: thesis: S₂[]
then A1: X is U -concatenation -unambiguous ;
let p1, q1, p2, q2 be U -valued FinSequence; :: thesis: ( p1 in X & p2 in X & p1 ^ q1 = p2 ^ q2 implies ( p1 = p2 & q1 = q2 ) )
A2: ( S₁[p1] & S₁[p2] & S₁[q1] & S₁[q2] ) by Lm1;
assume ( p1 in X & p2 in X ) ; :: thesis: ( not p1 ^ q1 = p2 ^ q2 or ( p1 = p2 & q1 = q2 ) )
then A3: ( p1 in X /\ (U *) & p2 in X /\ (U *) & q1 in U * & q2 in U * ) by A2, XBOOLE_0:def 4;
assume p1 ^ q1 = p2 ^ q2 ; :: thesis: ( p1 = p2 & q1 = q2 )
then (U -concatenation) . (p1,q1) = p2 ^ q2 by Th4
.= (U -concatenation) . (p2,q2) by Th4 ;
hence ( p1 = p2 & q1 = q2 ) by A1, A3; :: thesis: verum

end;

assume A4: S₂[] ; :: thesis: X is U -prefix

now :: thesis: for x1, x2, d1, d2 being set st x1 in X /\ (U *) & x2 in X /\ (U *) & d1 in U * & d2 in U * & (U -concatenation) . (x1,d1) = (U -concatenation) . (x2,d2) holds
( x1 = x2 & d1 = d2 )

let x1, x2, d1, d2 be set ; :: thesis: ( x1 in X /\ (U *) & x2 in X /\ (U *) & d1 in U * & d2 in U * & (U -concatenation) . (x1,d1) = (U -concatenation) . (x2,d2) implies ( x1 = x2 & d1 = d2 ) )
assume A5: ( x1 in X /\ (U *) & x2 in X /\ (U *) & d1 in U * & d2 in U * ) ; :: thesis: ( (U -concatenation) . (x1,d1) = (U -concatenation) . (x2,d2) implies ( x1 = x2 & d1 = d2 ) )
then reconsider x11 = x1, x22 = x2, d11 = d1, d22 = d2 as Element of U * ;
assume (U -concatenation) . (x1,d1) = (U -concatenation) . (x2,d2) ; :: thesis: ( x1 = x2 & d1 = d2 )
then x11 ^ d11 = (U -concatenation) . (x22,d22) by Th4
.= x22 ^ d22 by Th4 ;
hence ( x1 = x2 & d1 = d2 ) by A4, A5; :: thesis: verum

end;

hence X is U -prefix by Def10; :: thesis: verum