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

now :: thesis: ( t ^ <*n*> in dom T implies n + 1 in dom (t succ) )

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 Th7;
then n < len (t succ) by Def5;
then A1: n + 1 <= len (t succ) by NAT_1:13;
0 + 1 <= n + 1 by XREAL_1:6;
then n + 1 in Seg (len (t succ)) by A1, FINSEQ_1:1;
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 n + 1 <= len (t succ) by FINSEQ_1:1;
then n < len (t succ) by NAT_1:13;
then n < card (succ t) by Def5;
then t ^ <*n*> in succ t by Th7;
hence t ^ <*n*> in dom T ; :: thesis: verum