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

proof

hence
(T,x) <- T9 is D -valued
by RELAT_1:def 19; :: thesis: verum
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;

end;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;

end;

( 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 ;

end;hereby :: thesis: verum

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

( 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;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