let p, q, r be FinSequence; :: thesis: ( p ^ q is_a_prefix_of p ^ r implies q is_a_prefix_of r )
assume p ^ q is_a_prefix_of p ^ r ; :: thesis: q is_a_prefix_of r
then consider n being FinSequence such that
A1: p ^ r = (p ^ q) ^ n by TREES_1:1;
p ^ r = p ^ (q ^ n) by A1, FINSEQ_1:32;
then r = q ^ n by FINSEQ_1:33;
hence q is_a_prefix_of r by TREES_1:1; :: thesis: verum