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 A1, Th10;

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 A4, TREES_1:1, A3, A5;
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;

now :: thesis: not p <> p9

assume A12: p <> p9 ; :: thesis: contradiction
p,p9 are_c=-comparable by A8, A10, Th1;
hence contradiction by A6, A11, A12, TREES_1:def 10; :: thesis: verum

end;

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;