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 A2: ( q in dom (tree T,P,T1) & 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:
then consider t' being Element of dom T such that
A3: ( t' = q & ( for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t' ) ) ;

per cases by A2, Th13;

suppose A4: for p being FinSequence of NAT st p in P holds
( not p is_a_prefix_of q & (tree T,P,T1) . q = T . q ) ; :: thesis:

consider x being set such that
A5: x in P by A1, XBOOLE_0:def 1;
P c= dom T by TREES_1:def 14;
then reconsider x = x as Element of dom T by A5;
consider p' being FinSequence of NAT such that
A6: p' = x ;
thus (tree T,P,T1) . q = T . q by A4, A5, A6; :: thesis:

end;

suppose ex p, r being FinSequence of NAT st
( p in P & r in dom T1 & q = p ^ r & (tree T,P,T1) . q = T1 . r ) ; :: thesis:

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

end;