let p, q be FinSequence; :: thesis: ( p is_a_prefix_of q & len p = len q implies p = q )
assume A1: ( p is_a_prefix_of q & len p = len q ) ; :: thesis: p = q
then consider r being FinSequence such that
A2: q = p ^ r by Th8;
( len p = (len p) + (len r) & len p = 0 + (len p) ) by A1, A2, FINSEQ_1:35;
then r = {} ;
hence p = q by A2, FINSEQ_1:47; :: thesis: verum