let x be set ; :: thesis: for p1, p2 being FinSequence st p1 is_a_prefix_of p2 holds
p1 is_a_proper_prefix_of p2 ^ <*x*>
let p1, p2 be FinSequence; :: thesis: ( p1 is_a_prefix_of p2 implies p1 is_a_proper_prefix_of p2 ^ <*x*> )
assume A1: p1 is_a_prefix_of p2 ; :: thesis: p1 is_a_proper_prefix_of p2 ^ <*x*>
consider p3 being FinSequence such that
A2: p2 = p1 ^ p3 by A1, Th8;
A3: p2 ^ <*x*> = p1 ^ (p3 ^ <*x*>) by A2, FINSEQ_1:45;
thus p1 is_a_prefix_of p2 ^ <*x*> by A3, Th8; :: according to XBOOLE_0:def 8 :: thesis: not p1 = p2 ^ <*x*>
assume A4: p1 = p2 ^ <*x*> ; :: thesis: contradiction
A5: len p2 = (len (p2 ^ <*x*>)) + (len p3) by A2, A4, FINSEQ_1:35
.= ((len p2) + (len <*x*>)) + (len p3) by FINSEQ_1:35
.= ((len p2) + 1) + (len p3) by FINSEQ_1:56 ;
A6: (len p2) + 1 <= len p2 by A5, NAT_1:11;
thus contradiction by A6, NAT_1:13; :: thesis: verum