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 p1 ^ <*x*> is_a_prefix_of p2 ; :: thesis: p1 is_a_proper_prefix_of p2
then consider p3 being FinSequence such that
A1: p2 = (p1 ^ <*x*>) ^ p3 by Th1;
p2 = p1 ^ (<*x*> ^ p3) by A1, FINSEQ_1:32;
hence p1 is_a_prefix_of p2 by Th1; :: according to XBOOLE_0:def 8 :: thesis: not p1 = p2
assume p1 = p2 ; :: thesis: contradiction
then len p1 = (len (p1 ^ <*x*>)) + (len p3) by A1, FINSEQ_1:22
.= ((len p1) + (len <*x*>)) + (len p3) by FINSEQ_1:22
.= ((len p1) + 1) + (len p3) by FINSEQ_1:39 ;
then (len p1) + 1 <= len p1 by NAT_1:11;
hence contradiction by NAT_1:13; :: thesis: verum