set T2 = tree (T,P,T1);

let y be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not y in rng (tree (T,P,T1)) or y in D )

assume y in rng (tree (T,P,T1)) ; :: thesis: y in D

then consider x being object such that

A2: x in dom (tree (T,P,T1)) and

A3: y = (tree (T,P,T1)) . x by FUNCT_1:def 3;

x is Element of dom (tree (T,P,T1)) by A2;

then reconsider q = x as FinSequence of NAT ;

dom (tree (T,P,T1)) = tree ((dom T),P,(dom T1)) by Def2;

then A4: dom (tree (T,P,T1)) = { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t1 } \/ { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } by Th7;

let y be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not y in rng (tree (T,P,T1)) or y in D )

assume y in rng (tree (T,P,T1)) ; :: thesis: y in D

then consider x being object such that

A2: x in dom (tree (T,P,T1)) and

A3: y = (tree (T,P,T1)) . x by FUNCT_1:def 3;

x is Element of dom (tree (T,P,T1)) by A2;

then reconsider q = x as FinSequence of NAT ;

dom (tree (T,P,T1)) = tree ((dom T),P,(dom T1)) by Def2;

then A4: dom (tree (T,P,T1)) = { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t1 } \/ { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } by Th7;

per cases
( q in { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t1 } or q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } ) by A2, A4, XBOOLE_0:def 3;

end;

not p is_a_prefix_of t1 } or q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } ) by A2, A4, XBOOLE_0:def 3;

suppose A5:
q in { t1 where t1 is Element of dom T : for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t1 } ; :: thesis: y in D

not p is_a_prefix_of t1 } ; :: thesis: y in D

then A6:
(tree (T,P,T1)) . q = T . q
by A2, Th12;

rng T c= D by RELAT_1:def 19;

hence y in D by A7; :: thesis: verum

end;now :: thesis: q in dom T

then A7:
y in rng T
by A3, A6, FUNCT_1:def 3;
ex t9 being Element of dom T st

( q = t9 & ( for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t9 ) ) by A5;

hence q in dom T ; :: thesis: verum

end;( q = t9 & ( for p being FinSequence of NAT st p in P holds

not p is_a_prefix_of t9 ) ) by A5;

hence q in dom T ; :: thesis: verum

rng T c= D by RELAT_1:def 19;

hence y in D by A7; :: thesis: verum