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

proof

let y be set ; :: 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 set such that
A3: z in dom ((T,x) <- T9) and
A4: y = ((T,x) <- T9) . z by FUNCT_1:def 5;
reconsider z = z as Node of ((T,x) <- T9) by A3;
reconsider p9 = {} as Node of T9 by TREES_1:47;

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 A7: ((T,x) <- T9) . (p ^ p9) = T9 . p9 by Def7;
p ^ p9 = p by FINSEQ_1:47;
hence y in D by A4, A7; :: 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 A4; :: 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
A12: ( q in Leaves (dom T) & T . q = x & z = q ^ r ) ;
((T,x) <- T9) . z = T9 . r by A12, Def7;
hence y in D by A4; :: thesis: verum

end;

end;

end;

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