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 p' being Element of dom T ex r being Element of dom T1 st
( q = p' ^ r & p' 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 p' being Element of dom T ex r being Element of dom T1 st
( q = p' ^ r & p' 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 p' being Element of dom T ex r being Element of dom T1 st
( q = p' ^ r & p' in P & (tree T,P,T1) . q = T1 . r ) )
assume A1: ( 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 } ) ; :: thesis: ex p' being Element of dom T ex r being Element of dom T1 st
( q = p' ^ r & p' 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, Th13;

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

consider p' being Element of dom T, r being Element of dom T1 such that
A3: ( q = p' ^ r & p' in P ) by A1;

now

assume (tree T,P,T1) . q <> T1 . r ; :: thesis: contradiction
not p' is_a_prefix_of q by A2, A3;
hence contradiction by A3, TREES_1:8; :: thesis: verum

end;

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

then consider p, r being FinSequence of NAT such that
A4: ( p in P & r in dom T1 & q = p ^ r & (tree T,P,T1) . q = T1 . r ) ;
consider p' being Element of dom T, r' being Element of dom T1 such that
A5: ( q = p' ^ r' & p' in P ) by A1;

now

assume A6: p <> p' ; :: thesis: contradiction
p,p' are_c=-comparable by A4, A5, Th1;
hence contradiction by A4, A5, A6, TREES_1:def 13; :: thesis: verum

end;

hence ex p' being Element of dom T ex r being Element of dom T1 st
( q = p' ^ r & p' in P & (tree T,P,T1) . q = T1 . r ) by A4; :: thesis: verum

end;

end;