let T be finite-branching DecoratedTree; :: thesis: for x, x9 being Element of dom T st x9 in succ x holds
T . x9 in rng (succ (T,x))
let x, x9 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 Nat such that
A1: x9 = x ^ <*n*> and
x ^ <*n*> in dom T ;
A2: T . x9 = (succ (T,x)) . (n + 1) by A1, Th40;
dom (succ (T,x)) = dom (T * (x succ)) by Th36
.= dom (x succ) by Th37 ;
then n + 1 in dom (succ (T,x)) by A1, Th39;
hence T . x9 in rng (succ (T,x)) by A2, FUNCT_1:def 3; :: thesis: verum