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 & succ T,x = T * (q succ ) ) by TREES_9:def 6;
A3: n + 1 in dom (q succ ) by A1, A2, Th12;
then A4: n + 1 in dom (T * (q succ )) by Th10;
n + 1 in Seg (len (q succ )) by A3, FINSEQ_1:def 3;
then ( 1 <= n + 1 & n + 1 <= len (q succ ) ) by FINSEQ_1:3;
then A5: n < len (q succ ) by NAT_1:13;
(succ T,x) . (n + 1) = T . ((q succ ) . (n + 1)) by A2, A4, FUNCT_1:22
.= T . (x ^ <*n*>) by A2, A5, TREES_9:def 5 ;
hence T . (x ^ <*n*>) = (succ T,x) . (n + 1) ; :: thesis: verum