let p, q, r be FinSequence; :: thesis: ( not q is_a_prefix_of p ^ r or q is_a_prefix_of p or p is_a_prefix_of q )
given i being Nat such that Z0: q = (p ^ r) | (Seg i) ; :: according to TREES_1:def 1 :: thesis: ( q is_a_prefix_of p or p is_a_prefix_of q )

per cases ( len p <= i or len p >= i ) ;

suppose len p <= i ; :: thesis: ( q is_a_prefix_of p or p is_a_prefix_of q )

then consider j being Nat such that
A1: i = (len p) + j by NAT_1:10;
q = p ^ (r | (Seg j)) by Z0, A1, FINSEQ_6:14;
hence ( q is_a_prefix_of p or p is_a_prefix_of q ) by TREES_1:1; :: thesis: verum

end;

suppose len p >= i ; :: thesis: ( q is_a_prefix_of p or p is_a_prefix_of q )

then q = p | (Seg i) by Z0, LemP;
hence ( q is_a_prefix_of p or p is_a_prefix_of q ) by TREES_1:def 1; :: thesis: verum

end;

end;