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, Th41;
dom (succ (T,x)) = dom (T * (x succ)) by Th37
.= dom (x succ) by Th38 ;
then n + 1 in dom (succ (T,x)) by A1, Th40;
hence T . x9 in rng (succ (T,x)) by A2, FUNCT_1:def 3; :: thesis: verum