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