theorem Th39: :: TREES_3:39

for D1, D2 being non empty set
for T being DecoratedTree of D1,D2
for t being Element of dom T holds
( (T . t) `1 = (T `1) . t & (T `2) . t = (T . t) `2 )