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;
A4: len p = (len p) + (len r) by A2, A3, FINSEQ_1:35;
A5: r = {} by A4;
thus p = q by A3, A5, FINSEQ_1:47; :: thesis: verum