A1: rng (T,x <- T9) c= D

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (T,x <- T9) or y in D )
assume A2: y in rng (T,x <- T9) ; :: thesis: y in D
consider z being set such that
A3: z in dom (T,x <- T9) and
A4: y = (T,x <- T9) . z by A2, FUNCT_1:def 5;
reconsider z = z as Node of (T,x <- T9) by A3;
reconsider p9 = {} as Node of T9 by TREES_1:47;

per cases ( z in dom T or ex q being Node of T ex r being Node of T9 st
( q in Leaves (dom T) & T . q = x & z = q ^ r ) ) by Def7;

suppose A5: z in dom T ; :: thesis: y in D

reconsider p = z as Node of T by A5;

hereby :: thesis: verum

per cases ( ( p in Leaves (dom T) & T . p = x ) or not p in Leaves (dom T) or T . p <> x ) ;

suppose A6: ( p in Leaves (dom T) & T . p = x ) ; :: thesis: y in D

A7: (T,x <- T9) . (p ^ p9) = T9 . p9 by A6, Def7;
A8: p ^ p9 = p by FINSEQ_1:47;
thus y in D by A4, A7, A8; :: thesis: verum

end;

suppose A9: ( not p in Leaves (dom T) or T . p <> x ) ; :: thesis: y in D

A10: (T,x <- T9) . p = T . p by A9, Def7;
thus y in D by A4, A10; :: thesis: verum

end;

end;

end;

end;

suppose A11: ex q being Node of T ex r being Node of T9 st
( q in Leaves (dom T) & T . q = x & z = q ^ r ) ; :: thesis: y in D

consider q being Node of T, r being Node of T9 such that
A12: ( q in Leaves (dom T) & T . q = x & z = q ^ r ) by A11;
A13: (T,x <- T9) . z = T9 . r by A12, Def7;
thus y in D by A4, A13; :: thesis: verum

end;

end;

end;

thus T,x <- T9 is DecoratedTree of D by A1, RELAT_1:def 19; :: thesis: verum