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

proof

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

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 z in dom T ; :: thesis: y in D

then reconsider p = z as Node of T ;

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 ( p in Leaves (dom T) & T . p = x ) ; :: thesis: y in D

then A3: ((T,x) <- T9) . (p ^ p9) = T9 . p9 by Def7;
p ^ p9 = p by FINSEQ_1:34;
hence y in D by A2, A3; :: thesis: verum

end;

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

then ((T,x) <- T9) . p = T . p by Def7;
hence y in D by A2; :: thesis: verum

end;

end;

end;

end;

suppose 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

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

end;

end;

end;

hence (T,x) <- T9 is D -valued by RELAT_1:def 19; :: thesis: verum