let T be finite-branching DecoratedTree; :: thesis: for x being FinSequence
for n being Element of NAT st x ^ <*n*> in dom T holds
T . (x ^ <*n*>) = (succ T,x) . (n + 1)
let x be FinSequence; :: thesis: for n being Element of NAT st x ^ <*n*> in dom T holds
T . (x ^ <*n*>) = (succ T,x) . (n + 1)
let n be Element of 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:8;
then x in dom T by A1, TREES_1:45;
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, Th12;
then n + 1 in Seg (len (q succ )) by FINSEQ_1:def 3;
then n + 1 <= len (q succ ) by FINSEQ_1:3;
then A5: n < len (q succ ) by NAT_1:13;
n + 1 in dom (T * (q succ )) by A4, Th10;
then (succ T,x) . (n + 1) = T . ((q succ ) . (n + 1)) by A3, FUNCT_1:22
.= T . (x ^ <*n*>) by A2, A5, Def5 ;
hence T . (x ^ <*n*>) = (succ T,x) . (n + 1) ; :: thesis: verum