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