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:111;
assume ( not x in rng T or not x in Leaves T ) ; :: thesis: (T,x) <- T9 = T
then A2: not x in Leaves T by A1;
thus A3: 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) ) )
( 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;
hence ( ( 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 A2, FUNCT_1:def 6; :: 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 A3;
( p9 in Leaves (dom T) implies T . p9 in Leaves T ) by FUNCT_1:def 6;
hence ((T,x) <- T9) . p = T . p by A2, Def7; :: thesis: verum