let T be finite-branching DecoratedTree; :: thesis: for x being FinSequence
for n being Nat st x ^ <*n*> in dom T holds
T . (x ^ <*n*>) = (succ (T,x)) . (n + 1)
let x be FinSequence; :: thesis: for n being Nat st x ^ <*n*> in dom T holds
T . (x ^ <*n*>) = (succ (T,x)) . (n + 1)
let n be Nat; :: thesis: ( x ^ <*n*> in dom T implies T . (x ^ <*n*>) = (succ (T,x)) . (n + 1) )
assume A1: x ^ <*n*> in dom T ; :: thesis: T . (x ^ <*n*>) = (succ (T,x)) . (n + 1)
x is_a_prefix_of x ^ <*n*> by TREES_1:1;
then x in dom T by A1, TREES_1:20;
then consider q being Element of dom T such that
A2: q = x and
A3: succ (T,x) = T * (q succ) by Def6;
A4: n + 1 in dom (q succ) by A1, A2, Th39;
then n + 1 in Seg (len (q succ)) by FINSEQ_1:def 3;
then n + 1 <= len (q succ) by FINSEQ_1:1;
then A5: n < len (q succ) by NAT_1:13;
n + 1 in dom (T * (q succ)) by A4, Th37;
then (succ (T,x)) . (n + 1) = T . ((q succ) . (n + 1)) by A3, FUNCT_1:12
.= T . (x ^ <*n*>) by A2, A5, Def5 ;
hence T . (x ^ <*n*>) = (succ (T,x)) . (n + 1) ; :: thesis: verum