let T be Tree; :: thesis: for B being Branch of T
for t being Element of T st t in B & not B is finite holds
ex t9 being Element of T st
( t9 in B & t9 in succ t )
let B be Branch of T; :: thesis: for t being Element of T st t in B & not B is finite holds
ex t9 being Element of T st
( t9 in B & t9 in succ t )
let t be Element of T; :: thesis: ( t in B & not B is finite implies ex t9 being Element of T st
( t9 in B & t9 in succ t ) )
assume ( t in B & not B is finite ) ; :: thesis: ex t9 being Element of T st
( t9 in B & t9 in succ t )
then consider t99 being Element of T such that
A1: t99 in B and
A2: t is_a_proper_prefix_of t99 by Th50;
t is_a_prefix_of t99 by A2;
then consider r being FinSequence such that
A3: t99 = t ^ r by TREES_1:1;
reconsider r = r as FinSequence of NAT by A3, FINSEQ_1:36;
r | (Seg 1) is FinSequence of NAT by FINSEQ_1:18;
then consider r1 being FinSequence of NAT such that
A4: r1 = r | (Seg 1) ;
1 <= len r
proof
len t < len t99 by A2, TREES_1:6;
then consider m being Nat such that
A5: (len t) + m = len t99 by NAT_1:10;
m <> 0 by A2, A5, TREES_1:6;
then 0 < m ;
then A6: 0 + 1 <= m by NAT_1:13;
len t99 = (len t) + (len r) by A3, FINSEQ_1:22;
hence 1 <= len r by A5, A6; :: thesis: verum
end;
then consider n being Element of NAT such that
A7: r1 = <*n*> by A4, Th34;
A8: r1 is_a_prefix_of r by A4, TREES_1:def 1;
then A9: t ^ r1 is_a_prefix_of t99 by A3, FINSEQ_6:13;
t ^ <*n*> in T by A3, A7, A8, FINSEQ_6:13, TREES_1:20;
then consider t9 being Element of T such that
A10: t9 = t ^ <*n*> ;
t9 in succ t by A10;
hence ex t9 being Element of T st
( t9 in B & t9 in succ t ) by A1, A7, A9, A10, TREES_2:25; :: thesis: verum