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