let T, T1 be DecoratedTree; :: thesis: for P being AntiChain_of_Prefixes of dom T st P <> {} holds

for q being FinSequence of NAT holds

( not q in dom (tree (T,P,T1)) or 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 ) )

let P be AntiChain_of_Prefixes of dom T; :: thesis: ( P <> {} implies for q being FinSequence of NAT holds

( not q in dom (tree (T,P,T1)) or 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 ) ) )

assume A1: P <> {} ; :: thesis: for q being FinSequence of NAT holds

( not q in dom (tree (T,P,T1)) or 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 ) )

let q be FinSequence of NAT ; :: thesis: ( not q in dom (tree (T,P,T1)) or 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 ) )

assume q in dom (tree (T,P,T1)) ; :: thesis: ( 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 ) )

then q in tree ((dom T),P,(dom T1)) by A1, Def2;

hence ( 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 Def2; :: thesis: verum

for q being FinSequence of NAT holds

( not q in dom (tree (T,P,T1)) or 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 ) )

let P be AntiChain_of_Prefixes of dom T; :: thesis: ( P <> {} implies for q being FinSequence of NAT holds

( not q in dom (tree (T,P,T1)) or 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 ) ) )

assume A1: P <> {} ; :: thesis: for q being FinSequence of NAT holds

( not q in dom (tree (T,P,T1)) or 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 ) )

let q be FinSequence of NAT ; :: thesis: ( not q in dom (tree (T,P,T1)) or 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 ) )

assume q in dom (tree (T,P,T1)) ; :: thesis: ( 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 ) )

then q in tree ((dom T),P,(dom T1)) by A1, Def2;

hence ( 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 Def2; :: thesis: verum