let T be finite-branching DecoratedTree; :: thesis: for x9, x being Element of dom T st x9 in succ x holds
T . x9 in rng (succ T,x)
let x9, x be Element of dom T; :: thesis: ( x9 in succ x implies T . x9 in rng (succ T,x) )
assume x9 in succ x ; :: thesis: T . x9 in rng (succ T,x)
then consider n being Element of NAT such that
A1: x9 = x ^ <*n*> and
x ^ <*n*> in dom T ;
A2: T . x9 = (succ T,x) . (n + 1) by A1, Th13;
dom (succ T,x) = dom (T * (x succ )) by Th9
.= dom (x succ ) by Th10 ;
then n + 1 in dom (succ T,x) by A1, Th12;
hence T . x9 in rng (succ T,x) by A2, FUNCT_1:def 5; :: thesis: verum