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