let T, T1 be DecoratedTree; :: thesis: for P being AntiChain_of_Prefixes of dom T
for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } holds
ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

let P be AntiChain_of_Prefixes of dom T; :: thesis: for q being FinSequence of NAT st q in dom (tree (T,P,T1)) & q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } holds
ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

let q be FinSequence of NAT ; :: thesis: ( q in dom (tree (T,P,T1)) & q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } implies ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r ) )

assume that
A1: q in dom (tree (T,P,T1)) and
A2: q in { (p ^ s) where p is Element of dom T, s is Element of dom T1 : p in P } ; :: thesis: ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

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 A3: 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: ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

consider p9 being Element of dom T, r being Element of dom T1 such that
A4: q = p9 ^ r and
A5: p9 in P by A2;
(tree (T,P,T1)) . q = T1 . r by ;
hence ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r ) by A4, A5; :: 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: ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r )

then consider p, r being FinSequence of NAT such that
A6: p in P and
A7: r in dom T1 and
A8: q = p ^ r and
A9: (tree (T,P,T1)) . q = T1 . r ;
consider p9 being Element of dom T, r9 being Element of dom T1 such that
A10: q = p9 ^ r9 and
A11: p9 in P by A2;
hence ex p9 being Element of dom T ex r being Element of dom T1 st
( q = p9 ^ r & p9 in P & (tree (T,P,T1)) . q = T1 . r ) by A6, A7, A8, A9; :: thesis: verum
end;
end;