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 that
A1: p1 is_a_prefix_of p2 ^ <*x*> and
A2: p1 <> p2 ^ <*x*> ; :: according to XBOOLE_0:def 8 :: thesis: p1 is_a_prefix_of p2
A3: ex p3 being FinSequence st p2 ^ <*x*> = p1 ^ p3 by A1, Th1;
A4: len p1 <= len (p2 ^ <*x*>) by A1, NAT_1:43;
( len (p2 ^ <*x*>) = (len p2) + (len <*x*>) & len <*x*> = 1 ) by FINSEQ_1:22, FINSEQ_1:39;
then len p1 < (len p2) + 1 by A1, A2, A4, CARD_2:102, XXREAL_0:1;
then len p1 <= len p2 by NAT_1:13;
then ex p3 being FinSequence st p1 ^ p3 = p2 by A3, FINSEQ_1:47;
hence p1 is_a_prefix_of p2 by Th1; :: thesis: verum