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

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

(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 Node of ((T,x) <- T9); :: thesis: ((T,x) <- T9) . p = T . p
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;( 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

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