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 Th18;
reconsider s = p | (Seg (len q)) as FinSequence of NAT by FINSEQ_1:18;
len p = (len q) + (len r) by FINSEQ_1:22;
then len q <= len p by NAT_1:11;
then A2: len s = len q by FINSEQ_1:17;
now :: thesis: for n being Nat st 1 <= n & n <= len q holds
q . n = s . n
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) by FINSEQ_1:1;
Seg (len q) = dom q by FINSEQ_1:def 3;
then p . n = q . n by A3, FINSEQ_1:def 7;
hence q . n = s . n by A3, FUNCT_1:49; :: thesis: verum
end;
then q = s by A2, FINSEQ_1:14;
then A4: q is_a_prefix_of p ;
now :: thesis: ( q <> p implies q in T )
assume q <> p ; :: thesis: q in T
then q is_a_proper_prefix_of p by A4;
then A5: q in ProperPrefixes p by Def2;
ProperPrefixes p c= T by A1, Def3;
hence q in T by A5; :: thesis: verum
end;
hence q in T by A1; :: thesis: verum