let T, T1 be DecoratedTree; :: thesis:
let P be AntiChain_of_Prefixes of dom T; :: thesis:
assume A1: P <> {} ; :: thesis:
let q be FinSequence of NAT ; :: thesis:
assume that
A2: q in dom (tree (T,P,T1)) and
A3: 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:
A4: ex t9 being Element of dom T st
( t9 = q & ( for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t9 ) ) by A3;

consider x being object such that
A6: x in P by A1, XBOOLE_0:def 1;
P c= dom T by TREES_1:def 11;
then reconsider x = x as Element of dom T by A6;
ex p9 being FinSequence of NAT st p9 = x ;
hence (tree (T,P,T1)) . q = T . q by A5, A6; :: thesis:

end;

then consider p, r being FinSequence of NAT such that
A7: p in P and
r in dom T1 and
A8: q = p ^ r and
(tree (T,P,T1)) . q = T1 . r ;
not p is_a_prefix_of q by A4, A7;
hence (tree (T,P,T1)) . q = T . q by A8, TREES_1:1; :: thesis:

end;