let x be set ; :: thesis: for p1, p2 being FinSequence st p1 is_a_proper_prefix_of p2 ^ <*x*> holds
p1 is_a_prefix_of p2
let p1, p2 be FinSequence; :: thesis: ( p1 is_a_proper_prefix_of p2 ^ <*x*> implies p1 is_a_prefix_of p2 )
assume A1: ( p1 is_a_prefix_of p2 ^ <*x*> & p1 <> p2 ^ <*x*> ) ; :: according to XBOOLE_0:def 8 :: thesis: p1 is_a_prefix_of p2
then A2: ex p3 being FinSequence st p2 ^ <*x*> = p1 ^ p3 by Th8;
( len p1 <= len (p2 ^ <*x*>) & len p1 <> len (p2 ^ <*x*>) & len (p2 ^ <*x*>) = (len p2) + (len <*x*>) & len <*x*> = 1 ) by A1, Th15, FINSEQ_1:35, FINSEQ_1:56, NAT_1:44;
then len p1 < (len p2) + 1 by XXREAL_0:1;
then len p1 <= len p2 by NAT_1:13;
then ex p3 being FinSequence st p1 ^ p3 = p2 by A2, FINSEQ_1:64;
hence p1 is_a_prefix_of p2 by Th8; :: thesis: verum