let T, T' be DecoratedTree; :: thesis: for x being set st ( not x in rng T or not x in Leaves T ) holds
T,x <- T' = T
let x be set ; :: thesis: ( ( not x in rng T or not x in Leaves T ) implies T,x <- T' = 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 <- T' = T
A3: not x in Leaves T by A1, A2;
thus A4: dom (T,x <- T') = dom T :: according to TREES_4:def 1 :: thesis: for p being Node of (T,x <- T') holds (T,x <- T') . p = T . p

proof

let p be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not p in dom (T,x <- T') or p in dom T ) & ( not p in dom T or p in dom (T,x <- T') ) )
A5: ( p in dom (T,x <- T') iff ( p in dom T or ex q being Node of T ex r being Node of T' st
( q in Leaves (dom T) & T . q = x & p = q ^ r ) ) ) by Def7;
thus ( ( not p in dom (T,x <- T') or p in dom T ) & ( not p in dom T or p in dom (T,x <- T') ) ) by A3, A5, FUNCT_1:def 12; :: thesis: verum

end;

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