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