let w, s, t 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 ;
then consider a being FinSequence such that
A2: w ^ s = (w ^ t) ^ a by Th1;
(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 Th1;
hence t is_a_proper_prefix_of s by A1; :: thesis: verum