let x be set ; 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; ( 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*>
; XBOOLE_0:def 8 p1 is_a_prefix_of p2
A3:
ex p3 being FinSequence st p2 ^ <*x*> = p1 ^ p3
by A1, Th8;
A4:
len p1 <= len (p2 ^ <*x*>)
by A1, NAT_1:44;
A5:
( len (p2 ^ <*x*>) = (len p2) + (len <*x*>) & len <*x*> = 1 )
by FINSEQ_1:35, FINSEQ_1:56;
A6:
len p1 < (len p2) + 1
by A1, A2, A4, A5, Th15, XXREAL_0:1;
A7:
len p1 <= len p2
by A6, NAT_1:13;
A8:
ex p3 being FinSequence st p1 ^ p3 = p2
by A3, A7, FINSEQ_1:64;
thus
p1 is_a_prefix_of p2
by A8, Th8; verum