let it1, it2 be FinSequence; :: thesis: ( it1 is_a_prefix_of p & it1 is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds
r is_a_prefix_of it1 ) & it2 is_a_prefix_of p & it2 is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds
r is_a_prefix_of it2 ) implies it1 = it2 )
assume ( it1 c= p & it1 c= q & ( for r being FinSequence st r c= p & r c= q holds
r c= it1 ) & it2 c= p & it2 c= q & ( for r being FinSequence st r c= p & r c= q holds
r c= it2 ) ) ; :: thesis: it1 = it2
then ( it1 c= it2 & it2 c= it1 ) ;
hence it1 = it2 by XBOOLE_0:def 10; :: thesis: verum