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;
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 ;
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
then A6: (tree (T,P,T1)) . q = T . q by ;
now :: thesis: q in dom T
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;
then A7: y in rng T by ;
rng T c= D by RELAT_1:def 19;
hence y in D by A7; :: thesis: verum
end;
suppose q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } ; :: thesis: y in D
then ex p being Element of dom T ex r being Element of dom T1 st
( q = p ^ r & p in P & (tree (T,P,T1)) . q = T1 . r ) by ;
hence y in D by A3; :: thesis: verum
end;
end;