let c1, c2 be set ; :: thesis: for d being DecoratedTree st c1 <> c2 holds
((root-tree c1),c2) <- d = root-tree c1
let d be DecoratedTree; :: thesis: ( c1 <> c2 implies ((root-tree c1),c2) <- d = root-tree c1 )
assume A0: c1 <> c2 ; :: thesis: ((root-tree c1),c2) <- d = root-tree c1
AA: dom (((root-tree c1),c2) <- d) = dom (root-tree c1)

proof

let x be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis: ( ( not x in dom (((root-tree c1),c2) <- d) or x in dom (root-tree c1) ) & ( not x in dom (root-tree c1) or x in dom (((root-tree c1),c2) <- d) ) )

hereby :: thesis: ( not x in dom (root-tree c1) or x in dom (((root-tree c1),c2) <- d) )

assume x in dom (((root-tree c1),c2) <- d) ; :: thesis: x in dom (root-tree c1)
then reconsider p = x as Element of dom (((root-tree c1),c2) <- d) ;

per cases ( p in dom (root-tree c1) or ex q being Node of (root-tree c1) ex r being Node of d st
( q in Leaves (dom (root-tree c1)) & (root-tree c1) . q = c2 & p = q ^ r ) ) by TREES_4:def 7;

suppose p in dom (root-tree c1) ; :: thesis: x in dom (root-tree c1)

hence x in dom (root-tree c1) ; :: thesis: verum

end;

suppose ex q being Node of (root-tree c1) ex r being Node of d st
( q in Leaves (dom (root-tree c1)) & (root-tree c1) . q = c2 & p = q ^ r ) ; :: thesis: x in dom (root-tree c1)

then consider q being Node of (root-tree c1), r being Node of d such that
A2: ( q in Leaves (dom (root-tree c1)) & (root-tree c1) . q = c2 & p = q ^ r ) ;
thus x in dom (root-tree c1) by A2, A0; :: thesis: verum

end;

end;

end;

assume x in dom (root-tree c1) ; :: thesis: x in dom (((root-tree c1),c2) <- d)
hence x in dom (((root-tree c1),c2) <- d) by TREES_4:def 7; :: thesis: verum

end;

now :: thesis: for x being object st x in dom (root-tree c1) holds
(((root-tree c1),c2) <- d) . x = (root-tree c1) . x

let x be object ; :: thesis: ( x in dom (root-tree c1) implies (((root-tree c1),c2) <- d) . x = (root-tree c1) . x )
assume x in dom (root-tree c1) ; :: thesis: (((root-tree c1),c2) <- d) . x = (root-tree c1) . x
then reconsider p = x as Node of (root-tree c1) ;
(root-tree c1) . p = c1 ;
hence (((root-tree c1),c2) <- d) . x = (root-tree c1) . x by A0, TREES_4:def 7; :: thesis: verum

end;

hence ((root-tree c1),c2) <- d = root-tree c1 by AA, FUNCT_1:2; :: thesis: verum