theorem :: MSAFREE5:17

for c being set
for d, d1 being DecoratedTree holds dom d c= dom ((d,c) <- d1) by TREES_4:def 7;