theorem Th4: :: SCM_COMP:4
for s being State of SCM
for t being Terminal of SCM-AE holds (root-tree t) @ s = s . t