let q be FinSequence of NAT ; :: thesis: for T being Tree
for r being FinSequence st q ^ r in T holds
q in T
let T be Tree; :: thesis: for r being FinSequence st q ^ r in T holds
q in T
let r be FinSequence; :: thesis: ( q ^ r in T implies q in T )
assume A1: q ^ r in T ; :: thesis: q in T
then reconsider p = q ^ r as FinSequence of NAT by Th44;
reconsider s = p | (Seg (len q)) as FinSequence of NAT by FINSEQ_1:23;
len p = (len q) + (len r) by FINSEQ_1:35;
then len q <= len p by NAT_1:11;
then A2: ( len s = len q & Seg (len q) c= Seg (len p) ) by FINSEQ_1:7, FINSEQ_1:21;

now

let n be Nat; :: thesis: ( 1 <= n & n <= len q implies q . n = s . n )
assume ( 1 <= n & n <= len q ) ; :: thesis: q . n = s . n
then A3: ( n in Seg (len q) & Seg (len q) = dom q ) by FINSEQ_1:3, FINSEQ_1:def 3;
then ( p . n = q . n & n in Seg (len p) & dom p = Seg (len p) ) by A2, FINSEQ_1:def 3, FINSEQ_1:def 7;
hence q . n = s . n by A3, FUNCT_1:72; :: thesis: verum

end;

then q = s by A2, FINSEQ_1:18;
then A4: q is_a_prefix_of p by Def1;

now

assume q <> p ; :: thesis: q in T
then q is_a_proper_prefix_of p by A4, XBOOLE_0:def 8;
then ( q in ProperPrefixes p & ProperPrefixes p c= T ) by A1, Def4, Def5;
hence q in T ; :: thesis: verum

end;

hence q in T by A1; :: thesis: verum