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
reconsider p = q ^ r as FinSequence of NAT by A1, Th44;
reconsider s = p | (Seg (len q)) as FinSequence of NAT by FINSEQ_1:23;
A2: len p = (len q) + (len r) by FINSEQ_1:35;
A3: len q <= len p by A2, NAT_1:11;
A4: len s = len q by A3, FINSEQ_1:21;

A5: now

let n be Nat; :: thesis: ( 1 <= n & n <= len q implies q . n = s . n )
assume A6: ( 1 <= n & n <= len q ) ; :: thesis: q . n = s . n
A7: n in Seg (len q) by A6, FINSEQ_1:3;
A8: Seg (len q) = dom q by FINSEQ_1:def 3;
A9: p . n = q . n by A7, A8, FINSEQ_1:def 7;
thus q . n = s . n by A7, A9, FUNCT_1:72; :: thesis: verum

end;

A10: q = s by A4, A5, FINSEQ_1:18;
A11: q is_a_prefix_of p by A10, Def1;

A12: now

assume A13: q <> p ; :: thesis: q in T
A14: q is_a_proper_prefix_of p by A11, A13, XBOOLE_0:def 8;
A15: q in ProperPrefixes p by A14, Def4;
A16: ProperPrefixes p c= T by A1, Def5;
thus q in T by A15, A16; :: thesis: verum

end;

thus q in T by A1, A12; :: thesis: verum