let p2, p1 be FinSequence; :: thesis: ( ( {} is_a_proper_prefix_of p2 or {} <> p2 ) implies p1 is_a_proper_prefix_of p1 ^ p2 )
assume A1: ( {} is_a_proper_prefix_of p2 or {} <> p2 ) ; :: thesis: p1 is_a_proper_prefix_of p1 ^ p2
thus p1 is_a_prefix_of p1 ^ p2 by Th8; :: according to XBOOLE_0:def 8 :: thesis: not p1 = p1 ^ p2
assume p1 = p1 ^ p2 ; :: thesis: contradiction
then len p1 = (len p1) + (len p2) by FINSEQ_1:22;
then p2 = {} ;
hence contradiction by A1; :: thesis: verum