let T, T1 be DecoratedTree; :: thesis: for P being AntiChain_of_Prefixes of dom T st P <> {} holds
for q being FinSequence of NAT st 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 } holds
(tree T,P,T1) . q = T . q
let P be AntiChain_of_Prefixes of dom T; :: thesis: ( P <> {} implies for q being FinSequence of NAT st 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 } holds
(tree T,P,T1) . q = T . q )
assume A1: P <> {} ; :: thesis: for q being FinSequence of NAT st 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 } holds
(tree T,P,T1) . q = T . q
let q be FinSequence of NAT ; :: thesis: ( 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 } implies (tree T,P,T1) . q = T . q )
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: (tree T,P,T1) . q = T . q
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;

per cases ( 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 ) or 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 ) ) by A2, Th13;

suppose A5: 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: (tree T,P,T1) . q = T . q

consider x being set such that
A6: x in P by A1, XBOOLE_0:def 1;
A7: P c= dom T by TREES_1:def 14;
reconsider x = x as Element of dom T by A6, A7;
A8: ex p9 being FinSequence of NAT st p9 = x ;
thus (tree T,P,T1) . q = T . q by A5, A6, A8; :: thesis: verum

end;

suppose A9: 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: (tree T,P,T1) . q = T . q

consider p, r being FinSequence of NAT such that
A10: p in P and
r in dom T1 and
A11: q = p ^ r and
(tree T,P,T1) . q = T1 . r by A9;
A12: not p is_a_prefix_of q by A4, A10;
thus (tree T,P,T1) . q = T . q by A11, A12, TREES_1:8; :: thesis: verum

end;

end;