let T, T9 be DecoratedTree; :: thesis: for x being set st ( not x in rng T or not x in Leaves T ) holds
T,x <- T9 = T
let x be set ; :: thesis: ( ( not x in rng T or not x in Leaves T ) implies T,x <- T9 = T )
A1: Leaves T c= rng T by RELAT_1:144;
assume A2: ( not x in rng T or not x in Leaves T ) ; :: thesis: T,x <- T9 = T
A3: not x in Leaves T by A1, A2;
thus A4: dom (T,x <- T9) = dom T :: according to TREES_4:def 1 :: thesis: for p being Node of (T,x <- T9) holds (T,x <- T9) . p = T . p

proof

let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in dom (T,x <- T9) or p in dom T ) & ( not p in dom T or p in dom (T,x <- T9) ) )
A5: ( p in dom (T,x <- T9) iff ( p 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 & p = q ^ r ) ) ) by Def7;
thus ( ( not p in dom (T,x <- T9) or p in dom T ) & ( not p in dom T or p in dom (T,x <- T9) ) ) by A3, A5, FUNCT_1:def 12; :: thesis: verum

end;

let p be Node of (T,x <- T9); :: thesis: (T,x <- T9) . p = T . p
reconsider p9 = p as Node of T by A4;
A6: ( p9 in Leaves (dom T) implies T . p9 in Leaves T ) by FUNCT_1:def 12;
thus (T,x <- T9) . p = T . p by A3, A6, Def7; :: thesis: verum