let w, t, s be FinSequence; :: thesis: ( w ^ t is_a_proper_prefix_of w ^ s implies t is_a_proper_prefix_of s )
assume A1: w ^ t is_a_proper_prefix_of w ^ s ; :: thesis: t is_a_proper_prefix_of s
then w ^ t is_a_prefix_of w ^ s by XBOOLE_0:def 8;
then consider a being FinSequence such that
A2: w ^ s = (w ^ t) ^ a by Th8;
(w ^ t) ^ a = w ^ (t ^ a) by FINSEQ_1:32;
then s = t ^ a by A2, FINSEQ_1:33;
then t is_a_prefix_of s by Th8;
hence t is_a_proper_prefix_of s by A1, XBOOLE_0:def 8; :: thesis: verum