let T be finite-branching DecoratedTree; :: thesis: for t being Element of dom T
for n being Element of NAT holds
( t ^ <*n*> in dom T iff n + 1 in dom (t succ ) )
let t be Element of dom T; :: thesis: for n being Element of NAT holds
( t ^ <*n*> in dom T iff n + 1 in dom (t succ ) )
let n be Element of NAT ; :: thesis: ( t ^ <*n*> in dom T iff n + 1 in dom (t succ ) )

now

assume t ^ <*n*> in dom T ; :: thesis: n + 1 in dom (t succ )
then t ^ <*n*> in succ t ;
then n < card (succ t) by TREES_9:7;
then A1: n < len (t succ ) by TREES_9:def 5;
0 <= n by NAT_1:2;
then 0 + 1 <= n + 1 by XREAL_1:8;
then ( 1 <= n + 1 & n + 1 <= len (t succ ) ) by A1, NAT_1:13;
then n + 1 in Seg (len (t succ )) by FINSEQ_1:3;
hence n + 1 in dom (t succ ) by FINSEQ_1:def 3; :: thesis: verum

end;

hence ( t ^ <*n*> in dom T implies n + 1 in dom (t succ ) ) ; :: thesis: ( n + 1 in dom (t succ ) implies t ^ <*n*> in dom T )
assume n + 1 in dom (t succ ) ; :: thesis: t ^ <*n*> in dom T
then n + 1 in Seg (len (t succ )) by FINSEQ_1:def 3;
then ( 1 <= n + 1 & n + 1 <= len (t succ ) ) by FINSEQ_1:3;
then n < len (t succ ) by NAT_1:13;
then n < card (succ t) by TREES_9:def 5;
then t ^ <*n*> in succ t by TREES_9:7;
hence t ^ <*n*> in dom T ; :: thesis: verum