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 ;
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 object such that
A6: x in P by ;
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: verum
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: (tree (T,P,T1)) . q = T . q
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 ; :: thesis: verum
end;
end;